From 038ffcffc36cb82c8d807e9f40975a5c3762396d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Jan 2020 16:27:40 -0800
Subject: [PATCH] fix: `TacticM` should not see pending `syntheticMVars` from
 caller

---
 src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean b/src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean
index 0edcc1c251..ebb83b02a6 100644
--- a/src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean
+++ b/src/Init/Lean/Elab/SynthesizeSyntheticMVars.lean
@@ -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);