From c14ded6984a42e9bdc96c1cfa8246631ddbc6521 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 29 Dec 2019 10:04:44 -0800 Subject: [PATCH] fix: using incorrect context for `withDefault` --- src/Init/Lean/Elab/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index 7e20d02b14..4a6c8a5d6e 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -605,7 +605,7 @@ s ← get; let len := s.syntheticMVars.length; newSyntheticMVars ← s.syntheticMVars.filterM $ fun mvarDecl => match mvarDecl.kind with - | SyntheticMVarKind.withDefault defaultVal => do + | SyntheticMVarKind.withDefault defaultVal => withMVarContext mvarDecl.mvarId $ do val ← instantiateMVars mvarDecl.ref (mkMVar mvarDecl.mvarId); when val.getAppFn.isMVar $ unlessM (isDefEq mvarDecl.ref val defaultVal) $