diff options
| author | Frédéric Besson | 2020-03-23 10:15:47 +0100 |
|---|---|---|
| committer | Frédéric Besson | 2020-03-23 10:15:47 +0100 |
| commit | 8d0460a3235f1e98814924179681632bde7e6263 (patch) | |
| tree | 1bae6eb8afc1e27f961f39a0a4eb5f2473fc1cd4 | |
| parent | 7ba059507b67b1f6ea3566a5d1dee40f6af78316 (diff) | |
| parent | 76a4f90f4d52558590759ea86a122a2a287b9be2 (diff) | |
Merge PR #11442: Add module ZifyPow to avoid compatibility issue with 8.11.
Reviewed-by: fajb
| -rw-r--r-- | doc/changelog/04-tactics/11362-micromega-fix-11191.rst | 5 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 1 | ||||
| -rw-r--r-- | theories/micromega/ZifyPow.v | 1 |
3 files changed, 6 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). diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 60d6039b0f..67d0b37e81 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -50,6 +50,7 @@ theories/micromega/ZifyInst.v theories/micromega/ZifyBool.v theories/micromega/ZifyComparison.v theories/micromega/ZifyClasses.v +theories/micromega/ZifyPow.v theories/micromega/Zify.v theories/nsatz/Nsatz.v theories/omega/Omega.v diff --git a/theories/micromega/ZifyPow.v b/theories/micromega/ZifyPow.v new file mode 100644 index 0000000000..d208696c0f --- /dev/null +++ b/theories/micromega/ZifyPow.v @@ -0,0 +1 @@ +Require Export ZifyInst. |