chore: fix apply? error reporting when out of heartbeats

2026-03-17 18:34:06 +00:00 · 2024-11-19 11:36:14 +11:00
1 changed files with 1 additions and 1 deletions
--- a/src/Lean/Elab/Tactic/LibrarySearch.lean
+++ b/src/Lean/Elab/Tactic/LibrarySearch.lean
@@ -40,7 +40,7 @@ def exact? (ref : Syntax) (required : Option (Array (TSyntax `term))) (requireCl
    | some suggestions =>
      if requireClose then throwError
        "`exact?` could not close the goal. Try `apply?` to see partial suggestions."
-      reportOutOfHeartbeats `library_search ref
+      reportOutOfHeartbeats `apply? ref
      for (_, suggestionMCtx) in suggestions do
        withMCtx suggestionMCtx do
          addExactSuggestion ref (← instantiateMVars (mkMVar mvar)).headBeta (addSubgoalsMsg := true)