max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: missing withMVarContext

Browse source
This commit is contained in:
Leonardo de Moura 2020-08-14 12:52:51 -07:00
parent 50abd28f6e
commit c5316d5cf3
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/EqnCompiler/DepElim.lean
View file

@ -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;