diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean
index f6a423019d..8554a24bb5 100644
--- a/library/init/lean/compiler/ir/basic.lean
+++ b/library/init/lean/compiler/ir/basic.lean
@@ -398,60 +398,60 @@ partial def FnBody.isPure : FnBody → Bool
 abbrev IndexSet := RBTree Index Index.lt
 instance vsetInh : Inhabited IndexSet := ⟨{}⟩
 
-inductive ContextEntry
-| param     : IRType → ContextEntry
-| localVar  : IRType → Expr → ContextEntry
-| joinPoint : Array Param → FnBody → ContextEntry
+inductive LocalContextEntry
+| param     : IRType → LocalContextEntry
+| localVar  : IRType → Expr → LocalContextEntry
+| joinPoint : Array Param → FnBody → LocalContextEntry
 
-abbrev Context := RBMap Index ContextEntry Index.lt
+abbrev LocalContext := RBMap Index LocalContextEntry Index.lt
 
-def Context.addLocal (ctx : Context) (x : VarId) (t : IRType) (v : Expr) : Context :=
-ctx.insert x.idx (ContextEntry.localVar t v)
+def LocalContext.addLocal (ctx : LocalContext) (x : VarId) (t : IRType) (v : Expr) : LocalContext :=
+ctx.insert x.idx (LocalContextEntry.localVar t v)
 
-def Context.addJP (ctx : Context) (j : JoinPointId) (xs : Array Param) (b : FnBody) : Context :=
-ctx.insert j.idx (ContextEntry.joinPoint xs b)
+def LocalContext.addJP (ctx : LocalContext) (j : JoinPointId) (xs : Array Param) (b : FnBody) : LocalContext :=
+ctx.insert j.idx (LocalContextEntry.joinPoint xs b)
 
-def Context.addParam (ctx : Context) (p : Param) : Context :=
-ctx.insert p.x.idx (ContextEntry.param p.ty)
+def LocalContext.addParam (ctx : LocalContext) (p : Param) : LocalContext :=
+ctx.insert p.x.idx (LocalContextEntry.param p.ty)
 
-def Context.addParams (ctx : Context) (ps : Array Param) : Context :=
-ps.foldl Context.addParam ctx
+def LocalContext.addParams (ctx : LocalContext) (ps : Array Param) : LocalContext :=
+ps.foldl LocalContext.addParam ctx
 
-def Context.isJP (ctx : Context) (idx : Index) : Bool :=
+def LocalContext.isJP (ctx : LocalContext) (idx : Index) : Bool :=
 match ctx.find idx with
-| some (ContextEntry.joinPoint _ _) := true
+| some (LocalContextEntry.joinPoint _ _) := true
 | other := false
 
-def Context.getJPBody (ctx : Context) (j : JoinPointId) : Option FnBody :=
+def LocalContext.getJPBody (ctx : LocalContext) (j : JoinPointId) : Option FnBody :=
 match ctx.find j.idx with
-| some (ContextEntry.joinPoint _ b) := some b
+| some (LocalContextEntry.joinPoint _ b) := some b
 | other := none
 
-def Context.getJPParams (ctx : Context) (j : JoinPointId) : Option (Array Param) :=
+def LocalContext.getJPParams (ctx : LocalContext) (j : JoinPointId) : Option (Array Param) :=
 match ctx.find j.idx with
-| some (ContextEntry.joinPoint ys _) := some ys
+| some (LocalContextEntry.joinPoint ys _) := some ys
 | other := none
 
-def Context.isParam (ctx : Context) (idx : Index) : Bool :=
+def LocalContext.isParam (ctx : LocalContext) (idx : Index) : Bool :=
 match ctx.find idx with
-| some (ContextEntry.param _) := true
+| some (LocalContextEntry.param _) := true
 | other := false
 
-def Context.isLocalVar (ctx : Context) (idx : Index) : Bool :=
+def LocalContext.isLocalVar (ctx : LocalContext) (idx : Index) : Bool :=
 match ctx.find idx with
-| some (ContextEntry.localVar _ _) := true
+| some (LocalContextEntry.localVar _ _) := true
 | other := false
 
-def Context.contains (ctx : Context) (idx : Index) : Bool :=
+def LocalContext.contains (ctx : LocalContext) (idx : Index) : Bool :=
 ctx.contains idx
 
-def Context.eraseJoinPointDecl (ctx : Context) (j : JoinPointId) : Context :=
+def LocalContext.eraseJoinPointDecl (ctx : LocalContext) (j : JoinPointId) : LocalContext :=
 ctx.erase j.idx
 
-def Context.getType (ctx : Context) (x : VarId) : Option IRType :=
+def LocalContext.getType (ctx : LocalContext) (x : VarId) : Option IRType :=
 match ctx.find x.idx with
-| some (ContextEntry.param t) := some t
-| some (ContextEntry.localVar t _) := some t
+| some (LocalContextEntry.param t) := some t
+| some (LocalContextEntry.localVar t _) := some t
 | other := none
 
 abbrev IndexRenaming := RBMap Index Index Index.lt
diff --git a/library/init/lean/compiler/ir/boxing.lean b/library/init/lean/compiler/ir/boxing.lean
index 10bff0a765..ae0a9bcbef 100644
--- a/library/init/lean/compiler/ir/boxing.lean
+++ b/library/init/lean/compiler/ir/boxing.lean
@@ -48,7 +48,7 @@ def eqvTypes (t₁ t₂ : IRType) : Bool :=
 (t₁.isScalar == t₂.isScalar) && (!t₁.isScalar || t₁ == t₂)
 
 structure Env :=
-(ctx: Context) (resultType : IRType) (decls : FunId → Decl)
+(ctx: LocalContext) (resultType : IRType) (decls : FunId → Decl)
 
 abbrev M := ReaderT Env (StateT Index Id)
 
@@ -57,7 +57,7 @@ do idx ← getModify (+1),
    pure { idx := idx }
 
 def getEnv : M Env := read
-def getCtx : M Context := Env.ctx <$> getEnv
+def getCtx : M LocalContext := Env.ctx <$> getEnv
 def getResultType : M IRType := Env.resultType <$> getEnv
 def getVarType (x : VarId) : M IRType :=
 do ctx ← getCtx,
diff --git a/library/init/lean/compiler/ir/checker.lean b/library/init/lean/compiler/ir/checker.lean
index abe9eb1db7..bbf0695d92 100644
--- a/library/init/lean/compiler/ir/checker.lean
+++ b/library/init/lean/compiler/ir/checker.lean
@@ -11,7 +11,7 @@ namespace IR
 
 namespace Checker
 
-abbrev M := ExceptT String (ReaderT Context Id)
+abbrev M := ExceptT String (ReaderT LocalContext Id)
 
 def checkVar (x : VarId) : M Unit :=
 do ctx ← read,
@@ -67,7 +67,7 @@ def checkExpr (ty : IRType) : Expr → M Unit
 
 @[inline] def withParams (ps : Array Param) (k : M Unit) : M Unit :=
 do ctx ← read,
-   ctx ← ps.mfoldl (λ (ctx : Context) p, do
+   ctx ← ps.mfoldl (λ (ctx : LocalContext) p, do
       when (ctx.contains p.x.idx) $ throw ("invalid parameter declaration, shadowing is not allowed"),
       pure $ ctx.addParam p) ctx,
    adaptReader (λ _, ctx) k
@@ -79,12 +79,12 @@ partial def checkFnBody : FnBody → M Unit
   checkExpr t v,
   ctx ← read,
   when (ctx.contains x.idx) $ throw ("invalid variable declaration, shadowing is not allowed"),
-  adaptReader (λ ctx : Context, ctx.addLocal x t v) (checkFnBody b)
+  adaptReader (λ ctx : LocalContext, ctx.addLocal x t v) (checkFnBody b)
 | (FnBody.jdecl j ys v b) := do
   withParams ys (checkFnBody v),
   ctx ← read,
   when (ctx.contains j.idx) $ throw ("invalid join point declaration, shadowing is not allowed"),
-  adaptReader (λ ctx : Context, ctx.addJP j ys v) (checkFnBody b)
+  adaptReader (λ ctx : LocalContext, ctx.addJP j ys v) (checkFnBody b)
 | (FnBody.set x _ y b)      := checkVar x *> checkVar y *> checkFnBody b
 | (FnBody.uset x _ y b)     := checkVar x *> checkVar y *> checkFnBody b
 | (FnBody.sset x _ _ y _ b) := checkVar x *> checkVar y *> checkFnBody b
diff --git a/library/init/lean/compiler/ir/livevars.lean b/library/init/lean/compiler/ir/livevars.lean
index 416649d435..ea57ba5e0b 100644
--- a/library/init/lean/compiler/ir/livevars.lean
+++ b/library/init/lean/compiler/ir/livevars.lean
@@ -38,7 +38,7 @@ namespace IsLive
   Remark: we don't need to track local join points because we assume there is
   no variable or join point shadowing in our IR.
 -/
-abbrev M := State Context
+abbrev M := State LocalContext
 
 @[inline] def visitVar (w : Index) (x : VarId) : M Bool := pure (HasIndex.visitVar w x)
 @[inline] def visitJP (w : Index) (x : JoinPointId) : M Bool := pure (HasIndex.visitJP w x)
@@ -81,7 +81,7 @@ end IsLive
 
    Recall that we say that a join point `j` is free in `b` if `b` contains
    `FnBody.jmp j ys` and `j` is not local. -/
-def FnBody.hasLiveVar (b : FnBody) (ctx : Context) (x : VarId) : Bool :=
+def FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) : Bool :=
 (IsLive.visitFnBody x.idx b).run' ctx
 
 end IR
diff --git a/library/init/lean/compiler/ir/resetreuse.lean b/library/init/lean/compiler/ir/resetreuse.lean
index 5a2147bef2..5585a3526b 100644
--- a/library/init/lean/compiler/ir/resetreuse.lean
+++ b/library/init/lean/compiler/ir/resetreuse.lean
@@ -55,7 +55,7 @@ private partial def S (w : VarId) (c : CtorInfo) : FnBody → FnBody
     instr <;> S b
 
 /- We use `Context` to track join points in scope. -/
-abbrev M := ReaderT Context (StateT Index Id)
+abbrev M := ReaderT LocalContext (StateT Index Id)
 local attribute [instance] monadInhabited
 
 private def mkFresh : M VarId :=
@@ -87,7 +87,7 @@ private partial def Dmain (x : VarId) (c : CtorInfo) : FnBody → M (FnBody × B
     pure (FnBody.case tid y alts, true)
   else pure (e, false)
 | (FnBody.jdecl j ys v b) := do
-  (b, _) ← adaptReader (λ ctx : Context, ctx.addJP j ys v) (Dmain b),
+  (b, _) ← adaptReader (λ ctx : LocalContext, ctx.addJP j ys v) (Dmain b),
   (v, found) ← Dmain v,
   /- If `found == true`, then `Dmain b` must also have returned `(b, true)` since
      we assume the IR does not have dead join points. So, if `x` is live in `j`,
@@ -138,7 +138,7 @@ partial def R : FnBody → M FnBody
     pure $ FnBody.case tid x alts
 | (FnBody.jdecl j ys v b) := do
   v ← R v,
-  b ← adaptReader (λ ctx : Context, ctx.addJP j ys v) (R b),
+  b ← adaptReader (λ ctx : LocalContext, ctx.addJP j ys v) (R b),
   pure $ FnBody.jdecl j ys v b
 | e := do
   if e.isTerminal then pure e