From 76245b39d128da11c495bc8a42506808ad87b78a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 3 Jul 2022 15:38:48 -0700
Subject: [PATCH] chore: remove dead field

We have remove the old frontend a long time ago.
---
 src/Lean/MetavarContext.lean | 19 ++++++++-----------
 tests/lean/mvar1.lean        |  4 ++--
 tests/lean/mvar2.lean        |  2 +-
 3 files changed, 11 insertions(+), 14 deletions(-)

diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index c74303d6a5..ceafb60ddc 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -263,11 +263,8 @@ structure MetavarDecl where
   A delayed assignment for a metavariable `?m`. It represents an assignment of the form
   `?m := (fun fvars => val)`. The local context `lctx` provides the declarations for `fvars`.
   Note that `fvars` may not be defined in the local context for `?m`.
-
-  - TODO: after we delete the old frontend, we can remove the field `lctx`.
-    This field is only used in old C++ implementation. -/
+-/
 structure DelayedMetavarAssignment where
-  lctx     : LocalContext
   fvars    : Array Expr
   val      : Expr
 
@@ -395,8 +392,8 @@ def assignLevel (m : MetavarContext) (mvarId : MVarId) (val : Level) : MetavarCo
 def assignExpr (m : MetavarContext) (mvarId : MVarId) (val : Expr) : MetavarContext :=
   { m with eAssignment := m.eAssignment.insert mvarId val }
 
-def assignDelayed (m : MetavarContext) (mvarId : MVarId) (lctx : LocalContext) (fvars : Array Expr) (val : Expr) : MetavarContext :=
-  { m with dAssignment := m.dAssignment.insert mvarId { lctx, fvars, val } }
+def assignDelayed (m : MetavarContext) (mvarId : MVarId) (fvars : Array Expr) (val : Expr) : MetavarContext :=
+  { m with dAssignment := m.dAssignment.insert mvarId { fvars, val } }
 
 def getLevelAssignment? (m : MetavarContext) (mvarId : MVarId) : Option Level :=
   m.lAssignment.find? mvarId
@@ -963,7 +960,7 @@ mutual
 
          Remark: `newMVarKind != MetavarKind.syntheticOpaque ==> nestedFVars == #[]`
       -/
-      let rec cont (nestedFVars : Array Expr) (nestedLCtx : LocalContext) : M (Expr × Array Expr) := do
+      let rec cont (nestedFVars : Array Expr) : M (Expr × Array Expr) := do
         let args ← args.mapM (visit xs)
         let preserve ← preserveOrder
         -- Note that `toRevert` only contains free variables since it is the result of `getInScope`
@@ -984,15 +981,15 @@ mutual
             }
           match newMVarKind with
           | MetavarKind.syntheticOpaque =>
-            modify fun s => { s with mctx := assignDelayed s.mctx newMVarId nestedLCtx (toRevert ++ nestedFVars) (mkAppN (mkMVar mvarId) nestedFVars) }
+            modify fun s => { s with mctx := assignDelayed s.mctx newMVarId (toRevert ++ nestedFVars) (mkAppN (mkMVar mvarId) nestedFVars) }
           | _                           =>
             modify fun s => { s with mctx := assignExpr s.mctx mvarId result }
           return (mkAppN result args, toRevert)
       if !mvarDecl.kind.isSyntheticOpaque then
-        cont #[] mvarLCtx
+        cont #[]
       else match mctx.getDelayedAssignment? mvarId with
-      | none => cont #[] mvarLCtx
-      | some { fvars, lctx := nestedLCtx, .. } => cont fvars nestedLCtx -- Remark: nestedLCtx is bigger than mvarLCtx
+      | none => cont #[]
+      | some { fvars, .. } => cont fvars
 
   private partial def elimApp (xs : Array Expr) (f : Expr) (args : Array Expr) : M Expr := do
     match f with
diff --git a/tests/lean/mvar1.lean b/tests/lean/mvar1.lean
index a0f439dd12..1d6b1747c1 100644
--- a/tests/lean/mvar1.lean
+++ b/tests/lean/mvar1.lean
@@ -61,7 +61,7 @@ def mctx4  := mctx3.addExprMVarDecl `m3 `m3 lctx4 #[] natE
 def mctx5  := mctx4.addExprMVarDecl `m4 `m4 lctx1 #[] (arrow typeE (arrow natE (arrow α natE)))
 def mctx6  := mctx5.addExprMVarDecl `m5 `m5 lctx5 #[] typeE
 def mctx7  := mctx5.addExprMVarDecl `m6 `m6 lctx5 #[] (arrow typeE (arrow natE (arrow α natE)))
-def mctx8  := mctx7.assignDelayed `m4 lctx4 #[α, x, y] m3
+def mctx8  := mctx7.assignDelayed `m4 #[α, x, y] m3
 def mctx9  := mctx8.assignExpr `m3 (mkAppN g #[x, y])
 def mctx10 := mctx9.assignExpr `m1 a
 
@@ -90,7 +90,7 @@ partial def mkDiamond : Nat → Expr
 #eval toString (mctx7.instantiateMVars (mkDiamond 100)).1.getAppFn
 #eval toString (mctx10.instantiateMVars (mkDiamond 100)).1.getAppFn
 
-def mctx11 := mctx10.assignDelayed `m6 lctx5 #[α, x, y] m5
+def mctx11 := mctx10.assignDelayed `m6 #[α, x, y] m5
 def mctx12 := mctx11.assignExpr `m5 (arrow α α)
 
 def t4 := lctx6.mkLambda #[α, x, y, w] $ mkAppN f #[mkAppN m4 #[α, x, y], x]
diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean
index ae312a19fa..0a95888b24 100644
--- a/tests/lean/mvar2.lean
+++ b/tests/lean/mvar2.lean
@@ -50,7 +50,7 @@ def mctx1 : MetavarContext := {}
 def mctx2  := mctx1.addExprMVarDecl `m1 `m1 lctx1 #[] typeE
 def mctx3  := mctx2.addExprMVarDecl `m2 `m2 lctx3 #[] natE
 def mctx4  := mctx3.addExprMVarDecl `m3 `m3 lctx1 #[] (arrow typeE (arrow natE natE))
-def mctx5  := mctx4.assignDelayed `m3 lctx3 #[α, x] m2
+def mctx5  := mctx4.assignDelayed `m3 #[α, x] m2
 def mctx6  := mctx5.assignExpr `m2 (arrow α α)
 def mctx7  := mctx6.assignExpr `m1 natE