From e138fbf1e1cd95bfae05e17074f94a1ebde2edf8 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Sat, 18 Jan 2020 20:35:42 +0100 Subject: firstorder: default tactic is “auto with core” --- doc/changelog/04-tactics/11760-firstorder-leaf.rst | 9 +++++++++ doc/sphinx/proof-engine/tactics.rst | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/04-tactics/11760-firstorder-leaf.rst (limited to 'doc') 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 `_, + by Vincent Laporte). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index be185e885b..d498c1ee2c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4286,7 +4286,7 @@ some incompatibilities. :name: Firstorder Solver The default tactic used by :tacn:`firstorder` when no rule applies is - :g:`auto with *`, it can be reset locally or globally using this option. + :g:`auto with core`, it can be reset locally or globally using this option. .. cmd:: Print Firstorder Solver -- cgit v1.2.3