Pantograph/Frontend/MetaTranslate.lean

@@ -111,7 +111,7 @@ partial def translateLCtx : MetaTranslateM LocalContext := do
   let lctx ← MonadLCtx.getLCtx
   assert! lctx.isEmpty
   (← getSourceLCtx).foldlM (λ lctx srcLocalDecl => do
-    let localDecl ← Meta.withLCtx lctx #[] do
+    let localDecl ← Meta.withLCtx' lctx do
       translateLocalDecl srcLocalDecl
     pure $ lctx.addDecl localDecl
   ) lctx
@@ -148,7 +148,9 @@ def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab
   }) do
     let type := termInfo.expectedType?.get!
     let lctx' ← translateLCtx
+    --let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
     let mvar ← Meta.withLCtx lctx' #[] do
+      Meta.withLocalInstances (lctx'.decls.toList.filterMap id) do
       let type' ← translateExpr type
       trace[Pantograph.Frontend.MetaTranslate] "Translating from term info {← Meta.ppExpr type'}"
       Meta.mkFreshExprSyntheticOpaqueMVar type'

Test/Main.lean

@@ -1,4 +1,3 @@
-import LSpec
 import Test.Delate
 import Test.Environment
 import Test.Frontend
@@ -9,6 +8,8 @@ import Test.Proofs
 import Test.Serial
 import Test.Tactic
 
+import LSpec
+
 -- Test running infrastructure
 
 namespace Pantograph.Test