feat: do not recover

Author: leodemoura

src/Lean/Elab/Tactic/Grind/Basic.lean

@@ -354,7 +354,7 @@ def mkEvalTactic' (elaborator : Name) (params : Params) : TermElabM (Goal → TS
     -- **Note**: we discard changes to `Term.State`
     let (subgoals, grindState') ← Term.TermElabM.run' (ctx := termCtx) (s := termState) do
       let (_, s) ← GrindTacticM.run
-            (ctx := { methods, ctx := grindCtx, params, elaborator })
+            (ctx := { recover := false, methods, ctx := grindCtx, params, elaborator })
             (s := { state := grindState, goals := [goal] }) do
         evalGrindTactic stx.raw
         pruneSolvedGoals

src/Lean/Meta/Tactic/Grind/Action.lean

@@ -281,8 +281,11 @@ def checkSeqAt (s? : Option SavedState) (goal : Goal) (seq : List TGrind) : Grin
     s.restore
     -- **Note**: Ensure tracing is disabled.
     withTheReader Grind.Context (fun ctx => { ctx with config.trace := false }) do
-      let subgoals ← evalTactic goal tac
-      return subgoals.isEmpty
+      try
+        let subgoals ← evalTactic goal tac
+        return subgoals.isEmpty
+      catch _  =>
+        return false
 
 /--
 Helper action that checks whether the resulting tactic script produced by its continuation