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.
This commit is contained in:
parent
955fff52c5
commit
09b36c332a
1 changed files with 1 additions and 0 deletions
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue