diff options
Diffstat (limited to 'doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst')
| -rw-r--r-- | doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst | 7 |
1 files changed, 0 insertions, 7 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 deleted file mode 100644 index d510416990..0000000000 --- a/doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **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). |