diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 17e28744f0..bfe628e7fe 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -429,7 +429,7 @@ private def findTag? (gs : List MVarId) (tag : Name) : TacticM (Option MVarId) : let savedTag ← liftM $ getMVarTag g liftM $ setMVarTag g Name.anonymous try - evalTactic tac + closeUsingOrAdmit tac finally liftM $ setMVarTag g savedTag done