From 730b6aa3a3e1448e8eae89fd7ecee37f9c7fdb78 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Nov 2020 16:04:56 -0800
Subject: [PATCH] feat: admit goal when `case .. => ..` fails

---
 src/Lean/Elab/Tactic/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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