diff options
| author | Théo Zimmermann | 2020-01-22 17:31:19 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-01-22 17:31:19 +0100 |
| commit | 68421494cbd8d9e2bc8ab2482ee6f34a057b157a (patch) | |
| tree | 9f8a27be0ab34adacde38ffd6f97ecea049ab287 | |
| parent | 2b908101ab93303b20a41e9b69a5549109ec4603 (diff) | |
Insert changelog entry for #11430 from v8.11 branch.
| -rw-r--r-- | doc/sphinx/changes.rst | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 473015dea0..294f121cf8 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -573,10 +573,15 @@ Changes in 8.11.0 and `#11270 <https://github.com/coq/coq/issues/11270>`_, by Frédéric Besson). - **Deprecated:** The undocumented ``omega with`` tactic variant has been deprecated. - Using ``lia`` is the recommended replacement, tho the old semantics + Using :tacn:`lia` is the recommended replacement, tho the old semantics of ``omega with *`` can be recovered with ``zify; omega`` (`#11337 <https://github.com/coq/coq/pull/11337>`_, by Emilio Jesus Gallego Arias). +- **Fixed** + For compatibility reasons, in 8.11, :tacn:`zify` does not support :g:`Z.pow_pos` by default. + It can be enabled by loading explicitly the module :g:`ZifyPow`. + (`#11430 <https://github.com/coq/coq/pull/11430>`_ by Frédéric Besson + fixes `#11191 <https://github.com/coq/coq/issues/11191>`_). **Tactic language** |