From 09b36c332ad3dcaaba509a768b2108d16938e0ae Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Thu, 23 Oct 2025 17:08:06 -0700
Subject: [PATCH] fix: missing `processNewFacts` at solver tactics (#10938)

This PR ensures solver `grind` tactics (e.g., `ac`, `ring`, `lia`, etc)
process pending facts after making progress.
---
 src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean b/src/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
index fbf95a280e..2d2ac8224e 100644
--- 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