fix: missing processNewFacts at solver tactics

This PR ensures solver `grind` tactics (e.g., `ac`, `ring`, `lia`, etc) process pending facts after making progress.
2026-04-01 09:44:09 +00:00 · 2025-10-23 17:00:20 -07:00
1 changed files with 1 additions and 0 deletions
--- a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
@@ -102,6 +102,7 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
    let progress ← k
    unless progress do
      throwError "`{tacticName}` failed"
+    processNewFacts
    unless (← Grind.getConfig).verbose do
      return ()
    if (← get).inconsistent then