“auto with zarith”: use “lia” rather than “omega”

1 files changed, 7 insertions, 0 deletions

diff --git a/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst
new file mode 100644
index 0000000000..d510416990
--- /dev/null
+++ b/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst
@@ -0,0 +1,7 @@
+- **Changed:** The :g:`auto with zarith` tactic and variations (including :tacn:`intuition`)
+  may now call the :tacn:`lia` tactic instead of :tacn:`omega`
+  (when the `Omega` module is loaded);
+  more goals may be automatically solved,
+  fewer section variables will be captured spuriously
+  (`#11018 <https://github.com/coq/coq/pull/11018>`_,
+  by Vincent Laporte).