From 3b2605018be0ffcd763a17dbab34f12e01dee6d2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 Jan 2021 15:10:34 -0800 Subject: [PATCH] fix: propagate nested `LCtx` at `elimMVar` --- src/Lean/MetavarContext.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 775dc666b5..435fd7fb3c 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -885,7 +885,7 @@ mutual Remark: `newMVarKind != MetavarKind.syntheticOpaque ==> nestedFVars == #[]` -/ - let rec cont (nestedFVars : Array Expr) : M (Expr × Array Expr) := do + let rec cont (nestedFVars : Array Expr) (nestedLCtx : LocalContext) : M (Expr × Array Expr) := do let args ← args.mapM (visit xs) let preserve ← preserveOrder match collectDeps mctx mvarLCtx toRevert preserve with @@ -905,15 +905,15 @@ mutual } match newMVarKind with | MetavarKind.syntheticOpaque => - modify fun s => { s with mctx := assignDelayed s.mctx newMVarId mvarLCtx (toRevert ++ nestedFVars) (mkAppN (mkMVar mvarId) nestedFVars) } + modify fun s => { s with mctx := assignDelayed s.mctx newMVarId nestedLCtx (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 #[] + cont #[] mvarLCtx else match mctx.getDelayedAssignment? mvarId with - | none => cont #[] - | some { fvars := fvars, .. } => cont fvars + | none => cont #[] mvarLCtx + | some { fvars := fvars, lctx := nestedLCtx, .. } => cont fvars nestedLCtx -- Remark: nestedLCtx is bigger than mvarLCtx private partial def elimApp (xs : Array Expr) (f : Expr) (args : Array Expr) : M Expr := do match f with