diff options
Diffstat (limited to 'doc/changelog/04-tactics/11760-firstorder-leaf.rst')
| -rw-r--r-- | doc/changelog/04-tactics/11760-firstorder-leaf.rst | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/changelog/04-tactics/11760-firstorder-leaf.rst b/doc/changelog/04-tactics/11760-firstorder-leaf.rst new file mode 100644 index 0000000000..e6e4b827e5 --- /dev/null +++ b/doc/changelog/04-tactics/11760-firstorder-leaf.rst @@ -0,0 +1,9 @@ +- **Changed:** + The default tactic used by :g:`firstorder` is + :g:`auto with core` instead of :g:`auto with *`; + see :ref:`decisionprocedures` for details; + old behavior can be reset by using the `-compat 8.12` command-line flag; + to ease the migration of legacy code, the default solver can be set to `debug auto with *` + with `Set Firstorder Solver debug auto with *` + (`#11760 <https://github.com/coq/coq/pull/11760>`_, + by Vincent Laporte). |