diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/04-tactics/11362-micromega-fix-11191.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 2 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 2 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 1 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 2 |
5 files changed, 8 insertions, 4 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/sphinx/changes.rst b/doc/sphinx/changes.rst index a0cf9730a9..f76b60097a 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -4,7 +4,7 @@ Recent changes -------------- -.. ifconfig:: not coq_config.is_a_released_version +.. ifconfig:: not is_a_released_version .. include:: ../unreleased.rst diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index c2c1c68f5c..2ed9ec21b3 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -100,7 +100,7 @@ def copy_formatspecific_files(app): def setup(app): app.connect('builder-inited', copy_formatspecific_files) - app.add_config_value('coq_config', coq_config, 'env') + app.add_config_value('is_a_released_version', coq_config.is_a_released_version, 'env') # The master toctree document. # We create this file in `copy_master_doc` above. 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/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 84f32e187b..0b94b0d675 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -519,7 +519,7 @@ class ProductionObject(CoqObject): row = nodes.inline(classes=['prodn-row']) entry = nodes.inline(classes=['prodn-cell-nonterminal']) if lhs != "": - target_name = 'grammar-token-' + lhs + target_name = 'grammar-token-' + nodes.make_id(lhs) target = nodes.target('', '', ids=[target_name], names=[target_name]) # putting prodn-target on the target node won't appear in the tex file inline = nodes.inline(classes=['prodn-target']) |