From c5316d5cf3286b220688639da193d72494331ada Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 14 Aug 2020 12:52:51 -0700 Subject: [PATCH] fix: missing `withMVarContext` --- src/Lean/Meta/EqnCompiler/DepElim.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/EqnCompiler/DepElim.lean b/src/Lean/Meta/EqnCompiler/DepElim.lean index e515673c9b..51940686d2 100644 --- a/src/Lean/Meta/EqnCompiler/DepElim.lean +++ b/src/Lean/Meta/EqnCompiler/DepElim.lean @@ -463,7 +463,7 @@ match p.vars with | x :: xs => do subgoals ← cases p.mvarId x.fvarId!; subgoals.foldlM - (fun (s : State) subgoal => do + (fun (s : State) subgoal => withMVarContext subgoal.mvarId do let subst := subgoal.subst; let fields := subgoal.fields.toList; let newVars := fields ++ xs;