diff options
| author | Théo Zimmermann | 2020-01-22 19:24:48 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-21 19:04:02 +0100 |
| commit | 76a4f90f4d52558590759ea86a122a2a287b9be2 (patch) | |
| tree | 3641c9df54dfb9ddb0249ccdeb442a87cfe0eb6e /doc/changelog | |
| parent | 4d025d4161599ea20cd1dbf489a6412f019a7a7e (diff) | |
Add module ZifyPow to avoid compatibility issue with 8.11.
Also tweak the changelog entry to explain the difference.
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/04-tactics/11362-micromega-fix-11191.rst | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst index 79879c78d5..20d48929f2 100644 --- a/doc/changelog/04-tactics/11362-micromega-fix-11191.rst +++ b/doc/changelog/04-tactics/11362-micromega-fix-11191.rst @@ -1,5 +1,8 @@ - **Fixed:** - Regression of :tacn:`lia` due to more powerful :tacn:`zify` + :tacn:`zify` now handles :g:`Z.pow_pos` by default. + In Coq 8.11, this was the case only when loading module + :g:`ZifyPow` because this triggered a regression of :tacn:`lia`. + The regression is now fixed, and the module kept only for compatibility (`#11362 <https://github.com/coq/coq/pull/11362>`_, fixes `#11191 <https://github.com/coq/coq/issues/11191>`_, by Frédéric Besson). |