diff options
| author | Maxime Dénès | 2020-03-30 11:04:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2020-03-30 11:04:20 +0200 |
| commit | 454dfac256f43bf82a76eeaafb3ba8443db97d03 (patch) | |
| tree | 940e1b711a9f386362a0c20be7b1b46f5f9d2287 /doc | |
| parent | 668b3fbcf3387d6d3b450a4793695d0804685b05 (diff) | |
| parent | b99e95486d3f66c29cc831eb57c018c32b7479f5 (diff) | |
Merge PR #11018: “auto with zarith”: use “lia” rather than “omega”
Ack-by: Zimmi48
Reviewed-by: anton-trunov
Ack-by: jfehrle
Reviewed-by: maximedenes
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/11018-lia-in-auto-with-zarith.rst | 7 |
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). |