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

fix: TacticM should not see pending syntheticMVars from caller

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-19 16:27:40 -08:00
parent 0a3e9abccb
commit 038ffcffc3
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean
View file

@ -15,9 +15,10 @@ open Tactic (TacticM evalTactic getUnsolvedGoals)
def liftTacticElabM {α} (ref : Syntax) (mvarId : MVarId) (x : TacticM α) : TermElabM α :=
withMVarContext mvarId $ fun ctx s =>
match x { ref := ref, main := mvarId, .. ctx } { goals := [mvarId], .. s } with
| EStateM.Result.error ex newS => EStateM.Result.error (Term.Exception.ex ex) newS.toTermState
| EStateM.Result.ok a newS => EStateM.Result.ok a newS.toTermState
let savedSyntheticMVars := s.syntheticMVars;
match x { ref := ref, main := mvarId, .. ctx } { goals := [mvarId], syntheticMVars := [], .. s } with
| EStateM.Result.error ex newS => EStateM.Result.error (Term.Exception.ex ex) { syntheticMVars := savedSyntheticMVars, .. newS.toTermState }
| EStateM.Result.ok a newS => EStateM.Result.ok a { syntheticMVars := savedSyntheticMVars, .. newS.toTermState }
def ensureAssignmentHasNoMVars (ref : Syntax) (mvarId : MVarId) : TermElabM Unit := do
val ← instantiateMVars ref (mkMVar mvarId);