diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean index 1f6d45d..cd3f09b 100644 --- a/Pantograph/Frontend/MetaTranslate.lean +++ b/Pantograph/Frontend/MetaTranslate.lean @@ -148,7 +148,6 @@ 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