From b99e95486d3f66c29cc831eb57c018c32b7479f5 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 29 Oct 2019 16:18:00 +0000 Subject: “auto with zarith”: use “lia” rather than “omega” --- doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst (limited to 'doc') 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 `_, + by Vincent Laporte). -- cgit v1.2.3