Skip to content

Commit 09b36c3

Browse files
authored
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.
1 parent 955fff5 commit 09b36c3

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -102,6 +102,7 @@ def evalCheck (tacticName : Name) (k : GoalM Bool)
102102
let progress ← k
103103
unless progress do
104104
throwError "`{tacticName}` failed"
105+
processNewFacts
105106
unless (← Grind.getConfig).verbose do
106107
return ()
107108
if (← get).inconsistent then

0 commit comments

Comments
 (0)