diff options
| author | coqbot-app[bot] | 2020-12-04 08:29:55 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-04 08:29:55 +0000 |
| commit | b01b5fc9e56cf461d09d2884edefd232c9c63d6e (patch) | |
| tree | 3fe7ec71a6230638dd03bc9f58ded6157e239167 /doc | |
| parent | 88f23b3095c223966352b7d8c2d9990250f0c640 (diff) | |
| parent | d20e4edab5912eb41b8408c3c8ab7541f4fc7834 (diff) | |
Merge PR #13527: Changes for Coq 8.13
Reviewed-by: Zimmi48
Ack-by: jfehrle
Diffstat (limited to 'doc')
95 files changed, 699 insertions, 505 deletions
diff --git a/doc/changelog/01-kernel/00000-title.rst b/doc/changelog/01-kernel/00000-title.rst index f680628a05..287382eab0 100644 --- a/doc/changelog/01-kernel/00000-title.rst +++ b/doc/changelog/01-kernel/00000-title.rst @@ -1,3 +1,4 @@ -**Kernel** +Kernel +^^^^^^ diff --git a/doc/changelog/01-kernel/10390-uip.rst b/doc/changelog/01-kernel/10390-uip.rst deleted file mode 100644 index dab096d8db..0000000000 --- a/doc/changelog/01-kernel/10390-uip.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Definitional UIP, only when :flag:`Definitional UIP` is enabled. See - documentation of the flag for details. - (`#10390 <https://github.com/coq/coq/pull/10390>`_, - by Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/11604-persistent-arrays.rst b/doc/changelog/01-kernel/11604-persistent-arrays.rst deleted file mode 100644 index fbade033d2..0000000000 --- a/doc/changelog/01-kernel/11604-persistent-arrays.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Built-in support for persistent arrays, which expose a functional - interface but are implemented using an imperative data structure, for - better performance. - (`#11604 <https://github.com/coq/coq/pull/11604>`_, - by Maxime Dénès and Benjamin Grégoire, with help from Gaëtan Gilbert). diff --git a/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst b/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst deleted file mode 100644 index bec121836c..0000000000 --- a/doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - A loss of definitional equality for declarations obtained through - :cmd:`Include` when entering the scope of a :cmd:`Module` or - :cmd:`Module Type` was causing :cmd:`Search` not to see the included - declarations - (`#12537 <https://github.com/coq/coq/pull/12537>`_, fixes `#12525 - <https://github.com/coq/coq/pull/12525>`_ and `#12647 - <https://github.com/coq/coq/pull/12647>`_, by Hugo Herbelin). diff --git a/doc/changelog/01-kernel/13356-primarray-cumul.rst b/doc/changelog/01-kernel/13356-primarray-cumul.rst deleted file mode 100644 index 978ca325bf..0000000000 --- a/doc/changelog/01-kernel/13356-primarray-cumul.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** Primitive arrays are now irrelevant in their single - polymorphic universe (same as a polymorphic cumulative list - inductive would be) (`#13356 - <https://github.com/coq/coq/pull/13356>`_, fixes `#13354 - <https://github.com/coq/coq/issues/13354>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/00000-title.rst b/doc/changelog/02-specification-language/00000-title.rst index 99bd2c5b44..2d3e49a69d 100644 --- a/doc/changelog/02-specification-language/00000-title.rst +++ b/doc/changelog/02-specification-language/00000-title.rst @@ -1,3 +1,4 @@ -**Specification language, type inference** +Specification language, type inference +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/doc/changelog/02-specification-language/07825-rechable-from-evars.rst b/doc/changelog/02-specification-language/07825-rechable-from-evars.rst deleted file mode 100644 index e57d5a7bc5..0000000000 --- a/doc/changelog/02-specification-language/07825-rechable-from-evars.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - In :tacn:`refine`, new existential variables unified with existing ones are no - longer considered as fresh. The behavior of :tacn:`simple refine` no longer depends on - the orientation of evar-evar unification problems, and new existential variables - are always turned into (unshelved) goals. This can break compatibility in - some cases (`#7825 <https://github.com/coq/coq/pull/7825>`_, by Matthieu - Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and - Enrico Tassi, fixes `#4095 <https://github.com/coq/coq/issues/4095>`_ and - `#4413 <https://github.com/coq/coq/issues/4413>`_). diff --git a/doc/changelog/02-specification-language/10331-minim-prop-toset.rst b/doc/changelog/02-specification-language/10331-minim-prop-toset.rst deleted file mode 100644 index 6c442ca1aa..0000000000 --- a/doc/changelog/02-specification-language/10331-minim-prop-toset.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** Heuristics for universe minimization to :g:`Set`: also - use constraints ``Prop <= i`` (`#10331 - <https://github.com/coq/coq/pull/10331>`_, by Gaëtan Gilbert with - help from Maxime Dénès and Matthieu Sozeau, fixes `#12414 - <https://github.com/coq/coq/issues/12414>`_). diff --git a/doc/changelog/02-specification-language/12653-cumul-syntax.rst b/doc/changelog/02-specification-language/12653-cumul-syntax.rst deleted file mode 100644 index ba97f7c796..0000000000 --- a/doc/changelog/02-specification-language/12653-cumul-syntax.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now - support syntax `Inductive foo@{=i +j *k l}` to specify variance - information for their universes (in :ref:`Cumulative <cumulative>` - mode) (`#12653 <https://github.com/coq/coq/pull/12653>`_, by Gaëtan - Gilbert). diff --git a/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst b/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst deleted file mode 100644 index b0cf4ca4e3..0000000000 --- a/doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - Tweaked the algorithm giving default names to arguments. - Should reduce the frequency that argument names get an - unexpected suffix. - Also makes :flag:`Mangle Names` not mess up argument names. - (`#12756 <https://github.com/coq/coq/pull/12756>`_, - fixes `#12001 <https://github.com/coq/coq/issues/12001>`_ - and `#6785 <https://github.com/coq/coq/issues/6785>`_, - by Jasper Hugunin). diff --git a/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst b/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst deleted file mode 100644 index c9e941743c..0000000000 --- a/doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - Warning on unused variables in pattern-matching branches of - :n:`match` serving as catch-all branches for at least two distinct - patterns. - (`#12768 <https://github.com/coq/coq/pull/12768>`_, - fixes `#12762 <https://github.com/coq/coq/issues/12762>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst b/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst deleted file mode 100644 index 7fe69c39c1..0000000000 --- a/doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Removed:** - Undocumented and experimental forward class hint feature ``:>>``. - Use ``:>`` (see :n:`@of_type`) instead - (`#13106 <https://github.com/coq/coq/pull/13106>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst b/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst deleted file mode 100644 index 006989e6b3..0000000000 --- a/doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Implicit arguments taken into account in defined fields of a record type declaration - (`#13166 <https://github.com/coq/coq/pull/13166>`_, - fixes `#13165 <https://github.com/coq/coq/issues/13165>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13183-using-att.rst b/doc/changelog/02-specification-language/13183-using-att.rst deleted file mode 100644 index c380d932ed..0000000000 --- a/doc/changelog/02-specification-language/13183-using-att.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Definition and (Co)Fixpoint now support the :attr:`using` attribute. - It has the same effect as :cmd:`Proof using`, which is only available in - interactive mode. - (`#13183 <https://github.com/coq/coq/pull/13183>`_, - by Enrico Tassi). diff --git a/doc/changelog/02-specification-language/13188-instance-gen.rst b/doc/changelog/02-specification-language/13188-instance-gen.rst deleted file mode 100644 index 6a431f85ed..0000000000 --- a/doc/changelog/02-specification-language/13188-instance-gen.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Removed:** The type given to :cmd:`Instance` is no longer automatically - generalized over unbound and :ref:`generalizable <implicit-generalization>` variables. - Use :n:`Instance : \`{@type}` instead of :n:`Instance : @type` to get the old behaviour, or - enable the compatibility flag :flag:`Instance Generalized Output`. - (`#13188 <https://github.com/coq/coq/pull/13188>`_, fixes `#6042 - <https://github.com/coq/coq/issues/6042>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/13217-master+fix13216-typeclass-for-match-return-clause.rst b/doc/changelog/02-specification-language/13217-master+fix13216-typeclass-for-match-return-clause.rst deleted file mode 100644 index 2d8230b965..0000000000 --- a/doc/changelog/02-specification-language/13217-master+fix13216-typeclass-for-match-return-clause.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Allow use of type classes inference for the return predicate of a :n:`match` - (was deactivated in versions 8.10 to 8.12, `#13217 <https://github.com/coq/coq/pull/13217>`_, - fixes `#13216 <https://github.com/coq/coq/issues/13216>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst b/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst deleted file mode 100644 index bf792fda6d..0000000000 --- a/doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Inference of return predicate of a :g:`match` by inversion takes - sort elimination constraints into account - (`#13290 <https://github.com/coq/coq/pull/13290>`_, - grants `#13278 <https://github.com/coq/coq/issues/13278>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst b/doc/changelog/02-specification-language/13312-attributes+bool_single.rst deleted file mode 100644 index f069bc616b..0000000000 --- a/doc/changelog/02-specification-language/13312-attributes+bool_single.rst +++ /dev/null @@ -1,17 +0,0 @@ -- **Changed:** - :term:`Boolean attributes <boolean attribute>` are now specified using - key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`. - If the value is missing, the default is :n:`yes`. The old syntax is still - supported, but produces the ``deprecated-attribute-syntax`` warning. - - Deprecated attributes are :attr:`universes(monomorphic)`, - :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are - respectively replaced by :attr:`universes(polymorphic=no) <universes(polymorphic)>`, - :attr:`universes(template=no) <universes(template)>` - and :attr:`universes(cumulative=no) <universes(cumulative)>`. - Attributes :attr:`program` and :attr:`canonical` are also affected, - with the syntax :n:`@ident__attr(false)` being deprecated in favor of - :n:`@ident__attr=no`. - - (`#13312 <https://github.com/coq/coq/pull/13312>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst b/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst deleted file mode 100644 index 5758f35c3d..0000000000 --- a/doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - A case of unification raising an anomaly IllTypedInstance - (`#13376 <https://github.com/coq/coq/pull/13376>`_, - fixes `#13266 <https://github.com/coq/coq/issues/13266>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst b/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst deleted file mode 100644 index c0e5a81641..0000000000 --- a/doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Using :n:`{wf ...}` in local fixpoints is an error, not an anomaly - (`#13383 <https://github.com/coq/coq/pull/13383>`_, - fixes `#11816 <https://github.com/coq/coq/issues/11816>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst b/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst deleted file mode 100644 index 4bd214d7be..0000000000 --- a/doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - issue when two expressions involving different projections and one is - primitive need to be unified - (`#13386 <https://github.com/coq/coq/pull/13386>`_, - fixes `#9971 <https://github.com/coq/coq/issues/9971>`_, - by Hugo Herbelin). diff --git a/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst b/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst deleted file mode 100644 index eaf049dc97..0000000000 --- a/doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - A bug producing ill-typed instances of existential variables when let-ins - interleaved with assumptions - (`#13387 <https://github.com/coq/coq/pull/13387>`_, - fixes `#12348 <https://github.com/coq/coq/issues/13387>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/00000-title.rst b/doc/changelog/03-notations/00000-title.rst index abc532df11..0780bf9468 100644 --- a/doc/changelog/03-notations/00000-title.rst +++ b/doc/changelog/03-notations/00000-title.rst @@ -1,3 +1,4 @@ -**Notations** +Notations +^^^^^^^^^ diff --git a/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst deleted file mode 100644 index 8d681361e8..0000000000 --- a/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst +++ /dev/null @@ -1,13 +0,0 @@ -- **Changed:** - In notations (except in custom entries), the misleading :n:`@syntax_modifier` - :n:`@ident ident` (which accepted either an identifier or - a :g:`_`) is deprecated and should be replaced by :n:`@ident name`. If - the intent was really to only parse identifiers, this will - eventually become possible, but only as of Coq 8.15. - In custom entries, the meaning of :n:`@ident ident` is silently changed - from parsing identifiers or :g:`_` to parsing only identifiers - without warning, but this presumably affects only rare, recent and - relatively experimental code - (`#11841 <https://github.com/coq/coq/pull/11841>`_, - fixes `#9514 <https://github.com/coq/coq/pull/9514>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/11986-float-low-level-printing.rst b/doc/changelog/03-notations/11986-float-low-level-printing.rst deleted file mode 100644 index aba74891c6..0000000000 --- a/doc/changelog/03-notations/11986-float-low-level-printing.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - :flag:`Printing Float` flag to print primitive floats as hexadecimal - instead of decimal values. This is included in the :flag:`Printing All` flag - (`#11986 <https://github.com/coq/coq/pull/11986>`_, - by Pierre Roux). diff --git a/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst b/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst deleted file mode 100644 index e9b02aed6d..0000000000 --- a/doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - Improved support for notations/abbreviations with mixed terms and patterns (such as the forcing modality) - (`#12099 <https://github.com/coq/coq/pull/12099>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst b/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst deleted file mode 100644 index 5ea37e7494..0000000000 --- a/doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst +++ /dev/null @@ -1,19 +0,0 @@ -- **Deprecated** - ``Numeral.v`` is deprecated, please use ``Number.v`` instead. -- **Changed** - Rational and real constants are parsed differently. - The exponent is now encoded separately from the fractional part - using ``Z.pow_pos``. This way, parsing large exponents can no longer - blow up and constants are printed in a form closer to the one they - were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). -- **Removed** - OCaml parser and printer for real constants have been removed. - Real constants are now handled with proven Coq code. -- **Added:** - :ref:`Number Notation <number-notations>` and :ref:`String Notation - <string-notations>` commands now - support parameterized inductive and non inductive types - (`#12218 <https://github.com/coq/coq/pull/12218>`_, - fixes `#12035 <https://github.com/coq/coq/issues/12035>`_, - by Pierre Roux, review by Jason Gross and Jim Fehrle for the - reference manual). diff --git a/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst b/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst deleted file mode 100644 index 048835a0e9..0000000000 --- a/doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Scope information is propagated in indirect applications to a - reference prefixed with :g:`@@`; this covers for instance the case - :g:`r.(@@p) t` where scope information from :g:`p` is now taken into - account for interpreting :g:`t` (`#12685 - <https://github.com/coq/coq/pull/12685>`_, by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst b/doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst deleted file mode 100644 index 82cbefc60b..0000000000 --- a/doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` - (`#12765 <https://github.com/coq/coq/pull/12765>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst b/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst deleted file mode 100644 index 16fc91f911..0000000000 --- a/doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst +++ /dev/null @@ -1,10 +0,0 @@ -- **Changed:** - New model for ``only parsing`` and ``only printing`` notations with - support for at most one parsing-and-printing or only-parsing - notation per notation and scope, but an arbitrary number of - only-printing notations - (`#12950 <https://github.com/coq/coq/pull/12950>`_, - fixes `#4738 <https://github.com/coq/coq/issues/4738>`_ - and `#9682 <https://github.com/coq/coq/issues/9682>`_ - and part 2 of `#12908 <https://github.com/coq/coq/issues/12908>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst b/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst deleted file mode 100644 index fc909e7a1d..0000000000 --- a/doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Fixed:** - Issues in the presence of notations recursively referring to another - applicative notations, such as missing scope propagation, or failure - to use a notation for printing - (`#12960 <https://github.com/coq/coq/pull/12960>`_, - fixes `#9403 <https://github.com/coq/coq/issues/9403>`_ - and `#10803 <https://github.com/coq/coq/issues/10803>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst b/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst deleted file mode 100644 index e63ab9696e..0000000000 --- a/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Capture of the name of global references by - binders in the presence of notations for binders - (`#12965 <https://github.com/coq/coq/pull/12965>`_, - fixes `#9569 <https://github.com/coq/coq/issues/9569>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12979-doc-numbers.rst b/doc/changelog/03-notations/12979-doc-numbers.rst deleted file mode 100644 index 631bd6ec69..0000000000 --- a/doc/changelog/03-notations/12979-doc-numbers.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - :n:`Numeral Notation`, please use :ref:`Number Notation <number-notations>` instead. - (`#12979 <https://github.com/coq/coq/pull/12979>`_, - by Pierre Roux). diff --git a/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst b/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst deleted file mode 100644 index d472e6fdf0..0000000000 --- a/doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst +++ /dev/null @@ -1,12 +0,0 @@ -- **Changed:** - Redeclaring a notation reactivates also its printing rule; in - particular a second :cmd:`Import` of the same module reactivates the - printing rules declared in this module. In theory, this leads to - changes of behavior for printing. However, this is mitigated in - general by the adoption in `#12986 - <https://github.com/coq/coq/pull/12986>`_ of a priority given to - notations which match a larger part of the term to print - (`#12984 <https://github.com/coq/coq/pull/12984>`_, - fixes `#7443 <https://github.com/coq/coq/issues/7443>`_ - and `#10824 <https://github.com/coq/coq/issues/10824>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst b/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst deleted file mode 100644 index 8b233972bf..0000000000 --- a/doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Use of notations for printing now gives preference - to notations which match a larger part of the term to abbreviate - (`#12986 <https://github.com/coq/coq/pull/12986>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst b/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst deleted file mode 100644 index fb12c91729..0000000000 --- a/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** - Preventing notations for constructors to involve binders - (`#13092 <https://github.com/coq/coq/pull/13092>`_, - fixes `#13078 <https://github.com/coq/coq/issues/13078>`_, - by Hugo Herbelin). diff --git a/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst b/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst deleted file mode 100644 index c973e157dd..0000000000 --- a/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - The :n:`@binder` entry of :cmd:`Notation` can now be used in - notations expecting a single (non-recursive) binder - (`#13265 <https://github.com/coq/coq/pull/13265>`_, - by Hugo Herbelin, see section :n:`notations-and-binders` of the - reference manual). diff --git a/doc/changelog/03-notations/13415-intern-univs.rst b/doc/changelog/03-notations/13415-intern-univs.rst deleted file mode 100644 index e9f51461e5..0000000000 --- a/doc/changelog/03-notations/13415-intern-univs.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Fixed:** Notations understand universe names without getting - confused by different imported modules between declaration and use - locations (`#13415 <https://github.com/coq/coq/pull/13415>`_, fixes - `#13303 <https://github.com/coq/coq/issues/13303>`_, by Gaëtan - Gilbert). diff --git a/doc/changelog/04-tactics/00000-title.rst b/doc/changelog/04-tactics/00000-title.rst index 3c7802d632..afa7821f40 100644 --- a/doc/changelog/04-tactics/00000-title.rst +++ b/doc/changelog/04-tactics/00000-title.rst @@ -1,3 +1,4 @@ -**Tactics** +Tactics +^^^^^^^ diff --git a/doc/changelog/04-tactics/11906-micromega-booleans.rst b/doc/changelog/04-tactics/11906-micromega-booleans.rst deleted file mode 100644 index 39d1525ac3..0000000000 --- a/doc/changelog/04-tactics/11906-micromega-booleans.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - :tacn:`lia` is extended to deal with boolean operators e.g. `andb` or `Z.leb`. - (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) - (`#11906 <https://github.com/coq/coq/pull/11906>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst b/doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst deleted file mode 100644 index 15ab18dcf1..0000000000 --- a/doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - `apply in` supports several hypotheses - (`#12246 <https://github.com/coq/coq/pull/12246>`_, - by Hugo Herbelin; grants - `#9816 <https://github.com/coq/coq/pull/9816>`_). diff --git a/doc/changelog/04-tactics/12399-rm-prolog.rst b/doc/changelog/04-tactics/12399-rm-prolog.rst deleted file mode 100644 index afde7db370..0000000000 --- a/doc/changelog/04-tactics/12399-rm-prolog.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - The deprecated and undocumented "prolog" tactic was removed - (`#12399 <https://github.com/coq/coq/pull/12399>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/12423-rm-info.rst b/doc/changelog/04-tactics/12423-rm-info.rst deleted file mode 100644 index bf20453e6b..0000000000 --- a/doc/changelog/04-tactics/12423-rm-info.rst +++ /dev/null @@ -1,2 +0,0 @@ -- **Removed:** Removed info tactic that was deprecated in 8.5. - (`#12423 <https://github.com/coq/coq/pull/12423>`_, by Jim Fehrle). diff --git a/doc/changelog/04-tactics/12552-zify-pre-hook.rst b/doc/changelog/04-tactics/12552-zify-pre-hook.rst deleted file mode 100644 index 975c917b19..0000000000 --- a/doc/changelog/04-tactics/12552-zify-pre-hook.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Thhe :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` - tactic. (`#12552 <https://github.com/coq/coq/pull/12552>`_, - by Kazuhiko Sakaguchi). diff --git a/doc/changelog/04-tactics/12648-zify-int63.rst b/doc/changelog/04-tactics/12648-zify-int63.rst deleted file mode 100644 index ec7a1273e4..0000000000 --- a/doc/changelog/04-tactics/12648-zify-int63.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Added:** - The :tacn:`zify` tactic provides support for primitive integers (module :g:`ZifyInt63`). - (`#12648 <https://github.com/coq/coq/pull/12648>`_, by Frédéric Besson). diff --git a/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst deleted file mode 100644 index bc67fd025a..0000000000 --- a/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Giving an empty list of occurrences after :n:`in` in tactics is no - longer permitted. Omitting the :n:`in` gives the same behavior - (`#13237 <https://github.com/coq/coq/pull/13236>`_, - fixes `#13235 <https://github.com/coq/coq/issues/13235>`_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst b/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst deleted file mode 100644 index 089647a4b2..0000000000 --- a/doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - Avoiding exposing an internal name of the form :n:`_tmp` when applying the - :n:`_` introduction pattern would break a dependency - (`#13337 <https://github.com/coq/coq/pull/13337>`_, - fixes `#13336 <https://github.com/coq/coq/issues/13336>`_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst b/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst deleted file mode 100644 index c02129a33f..0000000000 --- a/doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - The case of tactics, such as :tacn:`eapply`, producing existential variables - under binders with an ill-formed instance - (`#13373 <https://github.com/coq/coq/pull/13373>`_, - fixes `#13363 <https://github.com/coq/coq/issues/13363>`_, - by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13381-bfs_eauto.rst b/doc/changelog/04-tactics/13381-bfs_eauto.rst deleted file mode 100644 index e63241e46c..0000000000 --- a/doc/changelog/04-tactics/13381-bfs_eauto.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Deprecated:** - Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new :tacn:`bfs eauto`. - Also deprecated 2-integer syntax for :tacn:`debug eauto` and :tacn:`info_eauto`. - (Use :tacn:`bfs eauto` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) - (`#13381 <https://github.com/coq/coq/pull/13381>`_, - by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13403-occs_nums_nat.rst b/doc/changelog/04-tactics/13403-occs_nums_nat.rst deleted file mode 100644 index 5dfa90a267..0000000000 --- a/doc/changelog/04-tactics/13403-occs_nums_nat.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Removed:** - :n:`at @occs_nums` clauses in tactics such as tacn:`unfold` - no longer allow negative values. A "-" before the - list (for set complement) is still supported. Ex: "at -1 -2" - is no longer supported but "at -1 2" is. - (`#13403 <https://github.com/coq/coq/pull/13403>`_, - by Jim Fehrle). diff --git a/doc/changelog/04-tactics/13417-no_int_or_var.rst b/doc/changelog/04-tactics/13417-no_int_or_var.rst deleted file mode 100644 index 667ee28eea..0000000000 --- a/doc/changelog/04-tactics/13417-no_int_or_var.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Removed:** - A number of tactics that formerly accepted negative - numbers as parameters now give syntax errors for negative - values. These include {e}constructor, do, timeout, - 9 {e}auto tactics and psatz*. - (`#13417 <https://github.com/coq/coq/pull/13417>`_, - by Jim Fehrle). diff --git a/doc/changelog/05-tactic-language/00000-title.rst b/doc/changelog/05-tactic-language/00000-title.rst index b34d190298..bc12b18b7d 100644 --- a/doc/changelog/05-tactic-language/00000-title.rst +++ b/doc/changelog/05-tactic-language/00000-title.rst @@ -1,3 +1,4 @@ -**Tactic language** +Tactic language +^^^^^^^^^^^^^^^ diff --git a/doc/changelog/05-tactic-language/13028-master+fix-quotations-printing.rst b/doc/changelog/05-tactic-language/13028-master+fix-quotations-printing.rst deleted file mode 100644 index a191716b2f..0000000000 --- a/doc/changelog/05-tactic-language/13028-master+fix-quotations-printing.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Fixed:** - printing of the quotation qualifiers when printing :g:`Ltac` functions - (`#13028 <https://github.com/coq/coq/pull/13028>`_, - fixes `#9716 <https://github.com/coq/coq/issues/9716>`_ - and `#13004 <https://github.com/coq/coq/issues/13004>`_, - by Hugo Herbelin). diff --git a/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst b/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst deleted file mode 100644 index d105561a23..0000000000 --- a/doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - An if-then-else syntax to Ltac2 - (`#13232 <https://github.com/coq/coq/pull/13232>`_, - fixes `#10110 <https://github.com/coq/coq/issues/10110>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/06-ssreflect/00000-title.rst b/doc/changelog/06-ssreflect/00000-title.rst index 2e724627ec..43cccd6d60 100644 --- a/doc/changelog/06-ssreflect/00000-title.rst +++ b/doc/changelog/06-ssreflect/00000-title.rst @@ -1,3 +1,4 @@ -**SSReflect** +SSReflect +^^^^^^^^^ diff --git a/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst b/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst deleted file mode 100644 index 8d1564533d..0000000000 --- a/doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - SSReflect intro pattern ltac views ``/[dup]``, ``/[swap]`` and ``/[apply]`` - (`#13317 <https://github.com/coq/coq/pull/13317>`_, - by Cyril Cohen). diff --git a/doc/changelog/06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst b/doc/changelog/06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst deleted file mode 100644 index e14ae89219..0000000000 --- a/doc/changelog/06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - Working around a bug of interaction between + and /(ltac:(...)) cf #13458 - (`#13459 <https://github.com/coq/coq/pull/13459>`_, - by Cyril Cohen). diff --git a/doc/changelog/07-commands-and-options/00000-title.rst b/doc/changelog/07-commands-and-options/00000-title.rst index 1a0272983e..fe50ae0e16 100644 --- a/doc/changelog/07-commands-and-options/00000-title.rst +++ b/doc/changelog/07-commands-and-options/00000-title.rst @@ -1,3 +1,4 @@ -**Commands and options** +Commands and options +^^^^^^^^^^^^^^^^^^^^ diff --git a/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst b/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst deleted file mode 100644 index 1c7c3102a3..0000000000 --- a/doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - :cmd:`Grab Existential Variables` and :cmd:`Existential` commands - (`#12516 <https://github.com/coq/coq/pull/12516>`_, - by Maxime Dénès). diff --git a/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst b/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst deleted file mode 100644 index c67b0f6e80..0000000000 --- a/doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. - Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 <https://github.com/coq/coq/pull/6261>`_ - (`#13016 <https://github.com/coq/coq/pull/13016>`_, by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst b/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst deleted file mode 100644 index 74818f8464..0000000000 --- a/doc/changelog/07-commands-and-options/13040-gc+best_fit.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - When compiled with OCaml >= 4.10.0, Coq will use the new best-fit GC - policy, which should provide some performance benefits. Coq's policy - is optimized for speed, but could increase memory consumption in - some cases. You are welcome to tune it using the ``OCAMLRUNPARAM`` - variable and report back setting so we could optimize more. - (`#13040 <https://github.com/coq/coq/pull/13040>`_, - fixes `#11277 <https://github.com/coq/coq/issues/11277>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst deleted file mode 100644 index 0ab9a58e6f..0000000000 --- a/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - Drop prefixes from grammar non-terminal names, - e.g. "constr:global" -> "global", "Prim.name" -> "name". - Visible in the output of :cmd:`Print Grammar` and :cmd:`Print Custom Grammar`. - (`#13096 <https://github.com/coq/coq/pull/13096>`_, - by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst b/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst deleted file mode 100644 index 1a6bc88c6c..0000000000 --- a/doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - When declaring arbitrary terms as hints, unsolved - evars are not abstracted implicitly anymore and instead - raise an error - (`#13139 <https://github.com/coq/coq/pull/13139>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst b/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst deleted file mode 100644 index 03be92f897..0000000000 --- a/doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Added:** - Added support for automatic insertion of coercions in :cmd:`Search` - patterns. Additionally, head patterns are now automatically - interpreted as types - (`#13255 <https://github.com/coq/coq/pull/13255>`_, - fixes `#13244 <https://github.com/coq/coq/issues/13244>`_, - by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst b/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst deleted file mode 100644 index 9ae759be56..0000000000 --- a/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - The :cmd:`Proof using` command can now be used without loading the - Ltac plugin (`-noinit` mode) - (`#13339 <https://github.com/coq/coq/pull/13339>`_, - by Théo Zimmermann). diff --git a/doc/changelog/07-commands-and-options/13345-master+doc-add-ml-path-not-exported.rst b/doc/changelog/07-commands-and-options/13345-master+doc-add-ml-path-not-exported.rst deleted file mode 100644 index dc8010b456..0000000000 --- a/doc/changelog/07-commands-and-options/13345-master+doc-add-ml-path-not-exported.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Clarify in the documentation that :cmd:`Add ML Path` is not exported to compiled files - (`#13345 <https://github.com/coq/coq/pull/13345>`_, - fixes `#13344 <https://github.com/coq/coq/issues/13344>`_, - by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/13352-cep-48.rst b/doc/changelog/07-commands-and-options/13352-cep-48.rst deleted file mode 100644 index cb2eeea74b..0000000000 --- a/doc/changelog/07-commands-and-options/13352-cep-48.rst +++ /dev/null @@ -1,12 +0,0 @@ -- **Changed:** - Option -native-compiler of the configure script now impacts the - default value of the option -native-compiler of coqc. The - -native-compiler option of the configure script is added an ondemand - value, which becomes the default, thus preserving the previous default - behavior. - The stdlib is still precompiled when configuring with -native-compiler - yes. It is not precompiled otherwise. - This an implementation of point 2 of - `CEP #48 <https://github.com/coq/ceps/pull/48>`_ - (`#13352 <https://github.com/coq/coq/pull/13352>`_, - by Pierre Roux). diff --git a/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst b/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst deleted file mode 100644 index 8ec7198b72..0000000000 --- a/doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Deprecated:** - The default value for hint locality is currently :attr:`local` in a section and - :attr:`global` otherwise, but is scheduled to change in a future release. For the - time being, adding hints outside of sections without specifying an explicit - locality is therefore triggering a deprecation warning. It is recommended to - use :attr:`export` whenever possible - (`#13384 <https://github.com/coq/coq/pull/13384>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst b/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst deleted file mode 100644 index df2bdfeabb..0000000000 --- a/doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Changed:** - The :attr:`export` locality can now be used for all Hint commands, - including Hint Cut, Hint Mode, Hint Transparent / Opaque and - Remove Hints - (`#13388 <https://github.com/coq/coq/pull/13388>`_, - by Pierre-Marie Pédrot). diff --git a/doc/changelog/08-tools/00000-title.rst b/doc/changelog/08-tools/00000-title.rst index bf462744fb..581585a8a7 100644 --- a/doc/changelog/08-tools/00000-title.rst +++ b/doc/changelog/08-tools/00000-title.rst @@ -1,3 +1,4 @@ -**Tools** +Tools +^^^^^ diff --git a/doc/changelog/08-tools/12389-coq_makefile.rst b/doc/changelog/08-tools/12389-coq_makefile.rst deleted file mode 100644 index 74e3a68170..0000000000 --- a/doc/changelog/08-tools/12389-coq_makefile.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Adding the possibility in coq_makefile to directly set the installation folders, - through the :n:`COQLIBINSTALL` and :n:`COQDOCINSTALL` variables. - See :ref:`coqmakefilelocal`. - (`#12389 <https://github.com/coq/coq/pull/12389>`_, by Martin Bodin, review of Enrico Tassi). diff --git a/doc/changelog/08-tools/12410-add-fixes.rst b/doc/changelog/08-tools/12410-add-fixes.rst deleted file mode 100644 index f4c41dc3c3..0000000000 --- a/doc/changelog/08-tools/12410-add-fixes.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Changed:** - ``dev/tools/make-changelog.sh`` now asks for a list of bugs fixed by the PR - (`#12410 <https://github.com/coq/coq/pull/12410>`_, fixes `#12386 - <https://github.com/coq/coq/issues/12386>`_, by Jason Gross). diff --git a/doc/changelog/08-tools/12613-coqchk-noi.rst b/doc/changelog/08-tools/12613-coqchk-noi.rst deleted file mode 100644 index b83c9c69a2..0000000000 --- a/doc/changelog/08-tools/12613-coqchk-noi.rst +++ /dev/null @@ -1,3 +0,0 @@ -- **Removed:** The option ``-I`` of coqchk was removed (it was - deprecated in Coq 8.8) (`#12613 - <https://github.com/coq/coq/pull/12613>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/08-tools/12862-more-mod-checking.rst b/doc/changelog/08-tools/12862-more-mod-checking.rst deleted file mode 100644 index bb1bf9e789..0000000000 --- a/doc/changelog/08-tools/12862-more-mod-checking.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - ``coqchk`` no longer reports names from inner modules of opaque modules as - axioms (`#12862 <https://github.com/coq/coq/pull/12862>`_, fixes `#12845 - <https://github.com/coq/coq/issues/12845>`_, by Jason Gross). diff --git a/doc/changelog/09-coqide/00000-title.rst b/doc/changelog/09-coqide/00000-title.rst index 0fc27cf380..81cf05b844 100644 --- a/doc/changelog/09-coqide/00000-title.rst +++ b/doc/changelog/09-coqide/00000-title.rst @@ -1,3 +1,4 @@ -**CoqIDE** +CoqIDE +^^^^^^ diff --git a/doc/changelog/09-coqide/12874-show_proof_diffs.rst b/doc/changelog/09-coqide/12874-show_proof_diffs.rst deleted file mode 100644 index 51bebad9be..0000000000 --- a/doc/changelog/09-coqide/12874-show_proof_diffs.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Support showing diffs for :cmd:`Show Proof` in CoqIDE from the :n:`View` menu. - See :ref:`showing_proof_diffs`. - (`#12874 <https://github.com/coq/coq/pull/12874>`_, - by Jim Fehrle and Enrico Tassi) diff --git a/doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst b/doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst deleted file mode 100644 index f7446cc5aa..0000000000 --- a/doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - Support for flag :flag:`Printing Goal Names` in View menu - (`#13145 <https://github.com/coq/coq/pull/13145>`_, - by Hugo Herbelin). diff --git a/doc/changelog/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst index d517a0e709..f636f48084 100644 --- a/doc/changelog/10-standard-library/00000-title.rst +++ b/doc/changelog/10-standard-library/00000-title.rst @@ -1,3 +1,4 @@ -**Standard library** +Standard library +^^^^^^^^^^^^^^^^ diff --git a/doc/changelog/10-standard-library/12094-app_inj_tail.rst b/doc/changelog/10-standard-library/12094-app_inj_tail.rst deleted file mode 100644 index 702fbb3d64..0000000000 --- a/doc/changelog/10-standard-library/12094-app_inj_tail.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Added:** - Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. - (`#12094 <https://github.com/coq/coq/pull/12094>`_, - fixes `#12093 <https://github.com/coq/coq/issues/12093>`_, - by Edward Wang). diff --git a/doc/changelog/10-standard-library/12186-creal-new-modulus.rst b/doc/changelog/10-standard-library/12186-creal-new-modulus.rst deleted file mode 100644 index 778bf78d59..0000000000 --- a/doc/changelog/10-standard-library/12186-creal-new-modulus.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - In the reals theory changed the epsilon in the definition of the modulus of convergence for CReal from 1/n (n in positive) to 2^z (z in Z) - so that a precision coarser than one is possible. Also added an upper bound to CReal to enable more efficient computations. - (`#12186 <https://github.com/coq/coq/pull/12186>`_, - by Michael Soegtrop). diff --git a/doc/changelog/10-standard-library/12420-decidable.rst b/doc/changelog/10-standard-library/12420-decidable.rst deleted file mode 100644 index 6a4da91fa3..0000000000 --- a/doc/changelog/10-standard-library/12420-decidable.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - ``Decidable`` instance for negation - (`#12420 <https://github.com/coq/coq/pull/12420>`_, - by Yishuai Li). diff --git a/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst b/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst deleted file mode 100644 index 208855b4c8..0000000000 --- a/doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - Int63 notations now match up with the rest of the standard library: :g:`a \% - m`, :g:`m == n`, :g:`m < n`, :g:`m <= n`, and :g:`m ≤ n` have been replaced - with :g:`a mod m`, :g:`m =? n`, :g:`m <? n`, :g:`m <=? n`, and :g:`m ≤? n`. - The old notations are still available as deprecated notations. Additionally, - there is now a ``Coq.Numbers.Cyclic.Int63.Int63.Int63Notations`` module that - users can import to get the ``Int63`` notations without unqualifying the - various primitives (`#12479 <https://github.com/coq/coq/pull/12479>`_, fixes - `#12454 <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst deleted file mode 100644 index 1709cf1eae..0000000000 --- a/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst +++ /dev/null @@ -1,9 +0,0 @@ -- **Changed:** - PrimFloat notations now match up with the rest of the standard library: :g:`m - == n`, :g:`m < n`, and :g:`m <= n` have been replaced with :g:`m =? n`, :g:`m - <? n`, and :g:`m <=? n`. The old notations are still available as deprecated - notations. Additionally, there is now a - ``Coq.Floats.PrimFloat.PrimFloatNotations`` module that users can import to - get the ``PrimFloat`` notations without unqualifying the various primitives - (`#12556 <https://github.com/coq/coq/pull/12556>`_, fixes `#12454 - <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). diff --git a/doc/changelog/10-standard-library/12716-curry.rst b/doc/changelog/10-standard-library/12716-curry.rst deleted file mode 100644 index 51b59e4a94..0000000000 --- a/doc/changelog/10-standard-library/12716-curry.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Deprecated:** - ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` - (`#12716 <https://github.com/coq/coq/pull/12716>`_, - by Yishuai Li). diff --git a/doc/changelog/10-standard-library/12799-list-repeat.rst b/doc/changelog/10-standard-library/12799-list-repeat.rst deleted file mode 100644 index adfc48f67b..0000000000 --- a/doc/changelog/10-standard-library/12799-list-repeat.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Added:** - New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat`` - (`#12799 <https://github.com/coq/coq/pull/12799>`_, - by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12801-cyclic-set.rst b/doc/changelog/10-standard-library/12801-cyclic-set.rst deleted file mode 100644 index 9a07d78144..0000000000 --- a/doc/changelog/10-standard-library/12801-cyclic-set.rst +++ /dev/null @@ -1,5 +0,0 @@ -- **Changed:** - Change the sort of cyclic numbers from Type to Set. For backward compatibility, a dynamic sort was defined in the 3 packages bignums, coqprime and color. - See for example commit 6f62bda in bignums. - (`#12801 <https://github.com/coq/coq/pull/12801>`_, - by Vincent Semeria). diff --git a/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst b/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst deleted file mode 100644 index 41359098e3..0000000000 --- a/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Changed:** - ``Require Import Coq.nsatz.NsatzTactic`` now allows using :tacn:`nsatz` - with `Z` and `Q` without having to supply instances or using ``Require Import Coq.nsatz.Nsatz``, which - transitively requires unneeded files declaring axioms used in the reals - (`#12861 <https://github.com/coq/coq/pull/12861>`_, - fixes `#12860 <https://github.com/coq/coq/issues/12860>`_, - by Jason Gross). diff --git a/doc/changelog/10-standard-library/13365-axiom-free-wf.rst b/doc/changelog/10-standard-library/13365-axiom-free-wf.rst deleted file mode 100644 index 1fc40894eb..0000000000 --- a/doc/changelog/10-standard-library/13365-axiom-free-wf.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Fixed:** - `Coq.Program.Wf.Fix_F_inv` and `Coq.Program.Wf.Fix_eq` are now axiom-free. They no longer assume proof irrelevance. - (`#13365 <https://github.com/coq/coq/pull/13365>`_, - by Li-yao Xia). diff --git a/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst index 6b301f59d3..7358fe192f 100644 --- a/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst +++ b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst @@ -1,3 +1,4 @@ -**Infrastructure and dependencies** +Infrastructure and dependencies +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst b/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst deleted file mode 100644 index 3b34e11ff8..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst +++ /dev/null @@ -1,8 +0,0 @@ -- **Changed:** - Coq's core system now uses the `zarith <https://github.com/ocaml/Zarith>`_ - library, based on GNU's gmp instead of ``num`` which is - deprecated upstream. The custom ``bigint`` module is - not longer provided; note that the ``micromega`` still uses - ``num`` - (`#11742 <https://github.com/coq/coq/pull/11742>`_, - by Emilio Jesus Gallego Arias and Vicent Laporte). diff --git a/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst b/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst deleted file mode 100644 index c142eec561..0000000000 --- a/doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst +++ /dev/null @@ -1,4 +0,0 @@ -- **Removed:** - The `num` library is not linked to Coq anymore - (`#13007 <https://github.com/coq/coq/pull/13007>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/12-misc/00000-title.rst b/doc/changelog/12-misc/00000-title.rst index 5e709e2b27..1391ec2164 100644 --- a/doc/changelog/12-misc/00000-title.rst +++ b/doc/changelog/12-misc/00000-title.rst @@ -1,3 +1,4 @@ -**Miscellaneous** +Miscellaneous +^^^^^^^^^^^^^ diff --git a/doc/changelog/12-misc/12586-declare+typing_flags.rst b/doc/changelog/12-misc/12586-declare+typing_flags.rst deleted file mode 100644 index 52915ceee9..0000000000 --- a/doc/changelog/12-misc/12586-declare+typing_flags.rst +++ /dev/null @@ -1,6 +0,0 @@ -- **Added:** - Typing flags can now be specified per-constant / inductive, this - allows to fine-grain specify them from plugins or attributes. See - :ref:`controlling-typing-flags` for details on attribute syntax. - (`#12586 <https://github.com/coq/coq/pull/12586>`_, - by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 249c7794be..c2b32afea2 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -8,6 +8,679 @@ Recent changes .. include:: ../unreleased.rst +Version 8.13 +------------ + +Summary of changes +~~~~~~~~~~~~~~~~~~ + +Coq version 8.13 integrates many usability improvements, as well +as extensions of the core language. +The main changes include: + + - :ref:`Introduction <813PrimArrays>` of :ref:`primitive persistent arrays<primitive-arrays>` + in the core language, implemented using imperative persistent arrays. + - Introduction of :ref:`definitional proof irrelevance <813UIP>` for the equality type + defined in the SProp sort. + - Cumulative record and inductive type declarations can now + :ref:`specify <813VarianceDecl>` the variance of their universes. + - Various bugfixes and uniformization of behavior with respect to the use of + implicit arguments and the handling of existential variables in + declarations, unification and tactics. + - New warning for :ref:`unused variables <813UnusedVar>` in catch-all match + branches that match multiple distinct patterns. + - New :ref:`warning <813HintWarning>` for `Hint` commands outside + sections without a locality attribute, whose goal is to eventually + remove the fragile default behavior of importing hints only when + using `Require`. The recommended fix is to declare hints as `export`, + instead of the current default `global`, meaning that they are imported + through `Require Import` only, not `Require`. + See the following `rationale and guidelines <https://coq.discourse.group/t/change-of-default-locality-for-hint-commands-in-coq-8-13/1140>`_ + for details. + - General support for :ref:`boolean attributes <813BooleanAttrs>`. + - Many improvements to the handling of :ref:`notations <813Notations>`, + including number notations, recursive notations and notations with bindings. + A new algorithm chooses the most precise notation available to print an expression, + which might introduce changes in printing behavior. + - Tactic :ref:`improvements <813Tactics>` in :tacn:`lia` and its :tacn:`zify` preprocessing step, + now supporting reasoning on boolean operators such as :g:`Z.leb` and supporting + primitive integers :g:`Int63`. + - Typing flags can now be specified :ref:`per-constant / inductive <813TypingFlags>`. + - Improvements to the reference manual including updated syntax + descriptions that match Coq's grammar in several chapters, and splitting parts of + the tactics chapter to independent sections. + +See the `Changes in 8.13+beta1`_ section and following sections for the +detailed list of changes, including potentially breaking changes marked +with **Changed**. + +Coq's documentation is available at https://coq.github.io/doc/v8.13/refman (reference +manual), and https://coq.github.io/doc/v8.13/stdlib (documentation of +the standard library). Developer documentation of the ML API is available +at https://coq.github.io/doc/v8.13/api. + +Maxime Dénès, Emilio Jesús Gallego Arias, Gaëtan Gilbert, Michael +Soegtrop and Théo Zimmermann worked on maintaining and improving the +continuous integration system and package building infrastructure. + +Erik Martin-Dorel has maintained the `Coq Docker images +<https://hub.docker.com/r/coqorg/coq>`_ that are used in many Coq +projects for continuous integration. + +The OPAM repository for Coq packages has been maintained by +Guillaume Claret, Karl Palmskog, Matthieu Sozeau and Enrico Tassi with +contributions from many users. A list of packages is available at +https://coq.inria.fr/opam/www/. + +Our current 32 maintainers are Yves Bertot, Frédéric Besson, Tej +Chajed, Cyril Cohen, Pierre Corbineau, Pierre Courtieu, Maxime Dénès, +Jim Fehrle, Julien Forest, Emilio Jesús Gallego Arias, Gaëtan Gilbert, +Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, +Vincent Laporte, Olivier Laurent, Assia Mahboubi, Kenji Maillard, +Guillaume Melquiond, Pierre-Marie Pédrot, Clément Pit-Claudel, +Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, +Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia +and Théo Zimmermann. + +The 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric +Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed, +Cyril Cohen, Julien Coolen, Matthew Dempsky, Maxime Dénès, Andres Erbsen, +Jim Fehrle, Emilio Jesús Gallego Arias, Paolo G. Giarrusso, Attila Gáspár, Gaëtan Gilbert, +Jason Gross, Benjamin Grégoire, Hugo Herbelin, Wolf Honore, Jasper Hugunin, Ignat Insarov, +Ralf Jung, Fabian Kunze, Vincent Laporte, Olivier Laurent, Larry D. Lee Jr, +Thomas Letan, Yishuai Li, Xia Li-yao, James Lottes, Jean-Christophe Léchenet, +Kenji Maillard, Erik Martin-Dorel, Yusuke Matsushita, Guillaume Melquiond, +Carl Patenaude-Poulin, Clément Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, +Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Matthieu Sozeau, +Enrico Tassi, Anton Trunov, Edward Wang, Li-yao Xia, Beta Ziliani and Théo Zimmermann. + +The Coq community at large helped improve the design of this new version via +the GitHub issue and pull request system, the Coq development mailing list +coqdev@inria.fr, the coq-club@inria.fr mailing list, the `Discourse forum +<https://coq.discourse.group/>`_ and the `Coq Zulip chat <http://coq.zulipchat.com>`_. + +Version 8.13's development spanned 5 months from the release of +Coq 8.12.0. Enrico Tassi and Maxime Dénès are the release managers of Coq 8.13. +This release is the result of 400 merged PRs, closing ~100 issues. + +| Nantes, November 2020, +| Matthieu Sozeau for the Coq development team +| + + +Changes in 8.13+beta1 +~~~~~~~~~~~~~~~~~~~~~ + +.. contents:: + :local: + +Kernel +^^^^^^ + + .. _813UIP: + +- **Added:** + Definitional UIP, only when :flag:`Definitional UIP` is enabled. + This models definitional uniqueness of identity proofs for the equality + type in SProp. It is deactivated by default as it can lead to + non-termination in combination with impredicativity. + Use of this flag is also printed by :cmd:`Print Assumptions`. See + documentation of the flag for details. + (`#10390 <https://github.com/coq/coq/pull/10390>`_, + by Gaëtan Gilbert). + + .. _813PrimArrays: + +- **Added:** + Built-in support for persistent arrays, which expose a functional + interface but are implemented using an imperative data structure, for + better performance. + (`#11604 <https://github.com/coq/coq/pull/11604>`_, + by Maxime Dénès and Benjamin Grégoire, with help from Gaëtan Gilbert). + + Primitive arrays are irrelevant in their single + polymorphic universe (same as a polymorphic cumulative list + inductive would be) (`#13356 + <https://github.com/coq/coq/pull/13356>`_, fixes `#13354 + <https://github.com/coq/coq/issues/13354>`_, by Gaëtan Gilbert). + +- **Fixed:** + A loss of definitional equality for declarations obtained through + :cmd:`Include` when entering the scope of a :cmd:`Module` or + :cmd:`Module Type` was causing :cmd:`Search` not to see the included + declarations + (`#12537 <https://github.com/coq/coq/pull/12537>`_, fixes `#12525 + <https://github.com/coq/coq/pull/12525>`_ and `#12647 + <https://github.com/coq/coq/pull/12647>`_, by Hugo Herbelin). + +Specification language, type inference +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + + .. _813BooleanAttrs: + +- **Changed:** + :term:`Boolean attributes <boolean attribute>` are now specified using + key/value pairs, that is to say :n:`@ident__attr{? = {| yes | no } }`. + If the value is missing, the default is :n:`yes`. The old syntax is still + supported, but produces the ``deprecated-attribute-syntax`` warning. + + Deprecated attributes are :attr:`universes(monomorphic)`, + :attr:`universes(notemplate)` and :attr:`universes(noncumulative)`, which are + respectively replaced by :attr:`universes(polymorphic=no) <universes(polymorphic)>`, + :attr:`universes(template=no) <universes(template)>` + and :attr:`universes(cumulative=no) <universes(cumulative)>`. + Attributes :attr:`program` and :attr:`canonical` are also affected, + with the syntax :n:`@ident__attr(false)` being deprecated in favor of + :n:`@ident__attr=no`. + (`#13312 <https://github.com/coq/coq/pull/13312>`_, + by Emilio Jesus Gallego Arias). +- **Changed:** Heuristics for universe minimization to :g:`Set`: also + use constraints ``Prop <= i`` (`#10331 + <https://github.com/coq/coq/pull/10331>`_, by Gaëtan Gilbert with + help from Maxime Dénès and Matthieu Sozeau, fixes `#12414 + <https://github.com/coq/coq/issues/12414>`_). +- **Changed:** The type given to :cmd:`Instance` is no longer automatically + generalized over unbound and :ref:`generalizable <implicit-generalization>` variables. + Use ``Instance : `{type}`` instead of :n:`Instance : @type` to get the old behaviour, or + enable the compatibility flag :flag:`Instance Generalized Output`. + (`#13188 <https://github.com/coq/coq/pull/13188>`_, fixes `#6042 + <https://github.com/coq/coq/issues/6042>`_, by Gaëtan Gilbert). +- **Changed:** + Tweaked the algorithm giving default names to arguments. + Should reduce the frequency that argument names get an + unexpected suffix. + Also makes :flag:`Mangle Names` not mess up argument names. + (`#12756 <https://github.com/coq/coq/pull/12756>`_, + fixes `#12001 <https://github.com/coq/coq/issues/12001>`_ + and `#6785 <https://github.com/coq/coq/issues/6785>`_, + by Jasper Hugunin). +- **Removed:** + Undocumented and experimental forward class hint feature ``:>>``. + Use ``:>`` (see :n:`@of_type`) instead + (`#13106 <https://github.com/coq/coq/pull/13106>`_, + by Pierre-Marie Pédrot). + + .. _813VarianceDecl: + +- **Added:** Commands :cmd:`Inductive`, :cmd:`Record` and synonyms now + support syntax `Inductive foo@{=i +j *k l}` to specify variance + information for their universes (in :ref:`Cumulative <cumulative>` + mode) (`#12653 <https://github.com/coq/coq/pull/12653>`_, by Gaëtan + Gilbert). + + .. _813UnusedVar: + +- **Added:** + Warning on unused variables in pattern-matching branches of + :n:`match` serving as catch-all branches for at least two distinct + patterns. + (`#12768 <https://github.com/coq/coq/pull/12768>`_, + fixes `#12762 <https://github.com/coq/coq/issues/12762>`_, + by Hugo Herbelin). +- **Added:** + Definition and (Co)Fixpoint now support the :attr:`using` attribute. + It has the same effect as :cmd:`Proof using`, which is only available in + interactive mode. + (`#13183 <https://github.com/coq/coq/pull/13183>`_, + by Enrico Tassi). + + .. _813TypingFlags: + +- **Added:** + Typing flags can now be specified per-constant / inductive, this + allows to fine-grain specify them from plugins or attributes. See + :ref:`controlling-typing-flags` for details on attribute syntax. + (`#12586 <https://github.com/coq/coq/pull/12586>`_, + by Emilio Jesus Gallego Arias). + +- **Added:** + Inference of return predicate of a :g:`match` by inversion takes + sort elimination constraints into account + (`#13290 <https://github.com/coq/coq/pull/13290>`_, + grants `#13278 <https://github.com/coq/coq/issues/13278>`_, + by Hugo Herbelin). +- **Fixed:** + Implicit arguments taken into account in defined fields of a record type declaration + (`#13166 <https://github.com/coq/coq/pull/13166>`_, + fixes `#13165 <https://github.com/coq/coq/issues/13165>`_, + by Hugo Herbelin). +- **Fixed:** + Allow use of typeclass inference for the return predicate of a :n:`match` + (was deactivated in versions 8.10 to 8.12, `#13217 <https://github.com/coq/coq/pull/13217>`_, + fixes `#13216 <https://github.com/coq/coq/issues/13216>`_, + by Hugo Herbelin). +- **Fixed:** + A case of unification raising an anomaly IllTypedInstance + (`#13376 <https://github.com/coq/coq/pull/13376>`_, + fixes `#13266 <https://github.com/coq/coq/issues/13266>`_, + by Hugo Herbelin). +- **Fixed:** + Using :n:`{wf ...}` in local fixpoints is an error, not an anomaly + (`#13383 <https://github.com/coq/coq/pull/13383>`_, + fixes `#11816 <https://github.com/coq/coq/issues/11816>`_, + by Hugo Herbelin). +- **Fixed:** + Issue when two expressions involving different projections and one is + primitive need to be unified + (`#13386 <https://github.com/coq/coq/pull/13386>`_, + fixes `#9971 <https://github.com/coq/coq/issues/9971>`_, + by Hugo Herbelin). +- **Fixed:** + A bug producing ill-typed instances of existential variables when let-ins + interleaved with assumptions + (`#13387 <https://github.com/coq/coq/pull/13387>`_, + fixes `#12348 <https://github.com/coq/coq/issues/13387>`_, + by Hugo Herbelin). + + .. _813Notations: + +Notations +^^^^^^^^^ + +- **Changed:** + In notations (except in custom entries), the misleading :n:`@syntax_modifier` + :n:`@ident ident` (which accepted either an identifier or + a :g:`_`) is deprecated and should be replaced by :n:`@ident name`. If + the intent was really to only parse identifiers, this will + eventually become possible, but only as of Coq 8.15. + In custom entries, the meaning of :n:`@ident ident` is silently changed + from parsing identifiers or :g:`_` to parsing only identifiers + without warning, but this presumably affects only rare, recent and + relatively experimental code + (`#11841 <https://github.com/coq/coq/pull/11841>`_, + fixes `#9514 <https://github.com/coq/coq/pull/9514>`_, + by Hugo Herbelin). +- **Changed:** + Improved support for notations/abbreviations with mixed terms and patterns (such as the forcing modality) + (`#12099 <https://github.com/coq/coq/pull/12099>`_, + by Hugo Herbelin). +- **Changed** + Rational and real constants are parsed differently. + The exponent is now encoded separately from the fractional part + using ``Z.pow_pos``. This way, parsing large exponents can no longer + blow up and constants are printed in a form closer to the one in which they + were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + by Pierre Roux). +- **Changed:** + Scope information is propagated in indirect applications to a + reference prefixed with :g:`@`; this covers for instance the case + :g:`r.(@p) t` where scope information from :g:`p` is now taken into + account for interpreting :g:`t` (`#12685 + <https://github.com/coq/coq/pull/12685>`_, by Hugo Herbelin). +- **Changed:** + New model for ``only parsing`` and ``only printing`` notations with + support for at most one parsing-and-printing or only-parsing + notation per notation and scope, but an arbitrary number of + only-printing notations + (`#12950 <https://github.com/coq/coq/pull/12950>`_, + fixes `#4738 <https://github.com/coq/coq/issues/4738>`_ + and `#9682 <https://github.com/coq/coq/issues/9682>`_ + and part 2 of `#12908 <https://github.com/coq/coq/issues/12908>`_, + by Hugo Herbelin). +- **Changed:** + Redeclaring a notation also reactivates its printing rule; in + particular a second :cmd:`Import` of the same module reactivates the + printing rules declared in this module. In theory, this leads to + changes in behavior for printing. However, this is mitigated in + general by the adoption in `#12986 + <https://github.com/coq/coq/pull/12986>`_ of a priority given to + notations which match a larger part of the term to print + (`#12984 <https://github.com/coq/coq/pull/12984>`_, + fixes `#7443 <https://github.com/coq/coq/issues/7443>`_ + and `#10824 <https://github.com/coq/coq/issues/10824>`_, + by Hugo Herbelin). +- **Changed:** + Use of notations for printing now gives preference + to notations which match a larger part of the term to abbreviate + (`#12986 <https://github.com/coq/coq/pull/12986>`_, + by Hugo Herbelin). +- **Removed** + OCaml parser and printer for real constants have been removed. + Real constants are now handled with proven Coq code. + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + by Pierre Roux). +- **Deprecated** + ``Numeral.v`` is deprecated, please use ``Number.v`` instead. + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + by Pierre Roux). +- **Deprecated:** + `Numeral Notation`, please use :cmd:`Number Notation` instead + (`#12979 <https://github.com/coq/coq/pull/12979>`_, + by Pierre Roux). +- **Added:** + :flag:`Printing Float` flag to print primitive floats as hexadecimal + instead of decimal values. This is included in the :flag:`Printing All` flag + (`#11986 <https://github.com/coq/coq/pull/11986>`_, + by Pierre Roux). +- **Added:** + :ref:`Number Notation <number-notations>` and :ref:`String Notation + <string-notations>` commands now + support parameterized inductive and non inductive types + (`#12218 <https://github.com/coq/coq/pull/12218>`_, + fixes `#12035 <https://github.com/coq/coq/issues/12035>`_, + by Pierre Roux, review by Jason Gross and Jim Fehrle for the + reference manual). +- **Added:** + Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` + (`#12765 <https://github.com/coq/coq/pull/12765>`_, + by Hugo Herbelin). +- **Added:** + The :n:`@binder` entry of :cmd:`Notation` can now be used in + notations expecting a single (non-recursive) binder + (`#13265 <https://github.com/coq/coq/pull/13265>`_, + by Hugo Herbelin, see section :ref:`notations-and-binders` of the + reference manual). +- **Fixed:** + Issues in the presence of notations recursively referring to another + applicative notations, such as missing scope propagation, or failure + to use a notation for printing + (`#12960 <https://github.com/coq/coq/pull/12960>`_, + fixes `#9403 <https://github.com/coq/coq/issues/9403>`_ + and `#10803 <https://github.com/coq/coq/issues/10803>`_, + by Hugo Herbelin). +- **Fixed:** + Capture the names of global references by + binders in the presence of notations for binders + (`#12965 <https://github.com/coq/coq/pull/12965>`_, + fixes `#9569 <https://github.com/coq/coq/issues/9569>`_, + by Hugo Herbelin). +- **Fixed:** + Preventing notations for constructors to involve binders + (`#13092 <https://github.com/coq/coq/pull/13092>`_, + fixes `#13078 <https://github.com/coq/coq/issues/13078>`_, + by Hugo Herbelin). +- **Fixed:** Notations understand universe names without getting + confused by different imported modules between declaration and use + locations (`#13415 <https://github.com/coq/coq/pull/13415>`_, fixes + `#13303 <https://github.com/coq/coq/issues/13303>`_, by Gaëtan + Gilbert). + + .. _813Tactics: + +Tactics +^^^^^^^ + +- **Changed:** + In :tacn:`refine`, new existential variables unified with existing ones are no + longer considered as fresh. The behavior of :tacn:`simple refine` no longer depends on + the orientation of evar-evar unification problems, and new existential variables + are always turned into (unshelved) goals. This can break compatibility in + some cases (`#7825 <https://github.com/coq/coq/pull/7825>`_, by Matthieu + Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and + Enrico Tassi, fixes `#4095 <https://github.com/coq/coq/issues/4095>`_ and + `#4413 <https://github.com/coq/coq/issues/4413>`_). +- **Changed:** + Giving an empty list of occurrences after :n:`in` in tactics is no + longer permitted. Omitting the :n:`in` gives the same behavior + (`#13237 <https://github.com/coq/coq/pull/13236>`_, + fixes `#13235 <https://github.com/coq/coq/issues/13235>`_, + by Hugo Herbelin). +- **Removed:** + :n:`at @occs_nums` clauses in tactics such as :tacn:`unfold` + no longer allow negative values. A "-" before the + list (for set complement) is still supported. Ex: "at -1 -2" + is no longer supported but "at -1 2" is. + (`#13403 <https://github.com/coq/coq/pull/13403>`_, + by Jim Fehrle). +- **Removed:** + A number of tactics that formerly accepted negative + numbers as parameters now give syntax errors for negative + values. These include {e}constructor, do, timeout, + 9 {e}auto tactics and psatz*. + (`#13417 <https://github.com/coq/coq/pull/13417>`_, + by Jim Fehrle). +- **Removed:** + The deprecated and undocumented `prolog` tactic was removed + (`#12399 <https://github.com/coq/coq/pull/12399>`_, + by Pierre-Marie Pédrot). +- **Removed:** `info` tactic that was deprecated in 8.5. + (`#12423 <https://github.com/coq/coq/pull/12423>`_, by Jim Fehrle). +- **Deprecated:** + Undocumented :n:`eauto @nat_or_var @nat_or_var` syntax in favor of new :tacn:`bfs eauto`. + Also deprecated 2-integer syntax for :tacn:`debug eauto` and :tacn:`info_eauto`. + (Use :tacn:`bfs eauto` with the :flag:`Info Eauto` or :flag:`Debug Eauto` flags instead.) + (`#13381 <https://github.com/coq/coq/pull/13381>`_, + by Jim Fehrle). +- **Added:** + :tacn:`lia` is extended to deal with boolean operators e.g. `andb` or `Z.leb`. + (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) + (`#11906 <https://github.com/coq/coq/pull/11906>`_, by Frédéric Besson). +- **Added:** + :tacn:`apply … in` supports several hypotheses + (`#12246 <https://github.com/coq/coq/pull/12246>`_, + by Hugo Herbelin; grants + `#9816 <https://github.com/coq/coq/pull/9816>`_). +- **Added:** + The :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` + tactic. (`#12552 <https://github.com/coq/coq/pull/12552>`_, + by Kazuhiko Sakaguchi). +- **Added:** + The :tacn:`zify` tactic provides support for primitive integers (module :g:`ZifyInt63`). + (`#12648 <https://github.com/coq/coq/pull/12648>`_, by Frédéric Besson). +- **Fixed:** + Avoid exposing an internal name of the form :n:`_tmp` when applying the + :n:`_` introduction pattern which would break a dependency + (`#13337 <https://github.com/coq/coq/pull/13337>`_, + fixes `#13336 <https://github.com/coq/coq/issues/13336>`_, + by Hugo Herbelin). +- **Fixed:** + The case of tactics, such as :tacn:`eapply`, producing existential variables + under binders with an ill-formed instance + (`#13373 <https://github.com/coq/coq/pull/13373>`_, + fixes `#13363 <https://github.com/coq/coq/issues/13363>`_, + by Hugo Herbelin). + +Tactic language +^^^^^^^^^^^^^^^ + +- **Added:** + An if-then-else syntax to Ltac2 + (`#13232 <https://github.com/coq/coq/pull/13232>`_, + fixes `#10110 <https://github.com/coq/coq/issues/10110>`_, + by Pierre-Marie Pédrot). +- **Fixed:** + Printing of the quotation qualifiers when printing :g:`Ltac` functions + (`#13028 <https://github.com/coq/coq/pull/13028>`_, + fixes `#9716 <https://github.com/coq/coq/issues/9716>`_ + and `#13004 <https://github.com/coq/coq/issues/13004>`_, + by Hugo Herbelin). + +SSReflect +^^^^^^^^^ + +- **Added:** + SSReflect intro pattern ltac views ``/[dup]``, ``/[swap]`` and ``/[apply]`` + (`#13317 <https://github.com/coq/coq/pull/13317>`_, + by Cyril Cohen). +- **Fixed:** + Working around a bug of interaction between + and /(ltac:(...)) cf + `#13458 <https://github.com/coq/coq/issues/13458>`_ + (`#13459 <https://github.com/coq/coq/pull/13459>`_, + by Cyril Cohen). + +Commands and options +^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + Drop prefixes from grammar non-terminal names, + e.g. "constr:global" -> "global", "Prim.name" -> "name". + Visible in the output of :cmd:`Print Grammar` and :cmd:`Print Custom Grammar`. + (`#13096 <https://github.com/coq/coq/pull/13096>`_, + by Jim Fehrle). +- **Changed:** + When declaring arbitrary terms as hints, unsolved + evars are not abstracted implicitly anymore and instead + raise an error + (`#13139 <https://github.com/coq/coq/pull/13139>`_, + by Pierre-Marie Pédrot). +- **Removed:** + In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. + Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 <https://github.com/coq/coq/pull/6261>`_ + (`#13016 <https://github.com/coq/coq/pull/13016>`_, by Jim Fehrle). + + .. _813HintWarning: + +- **Deprecated:** + The default value for hint locality is currently :attr:`local` in a section and + :attr:`global` otherwise, but is scheduled to change in a future release. For the + time being, adding hints outside of sections without specifying an explicit + locality is therefore triggering a deprecation warning. It is recommended to + use :attr:`export` whenever possible + (`#13384 <https://github.com/coq/coq/pull/13384>`_, + by Pierre-Marie Pédrot). +- **Deprecated:** + :cmd:`Grab Existential Variables` and :cmd:`Existential` commands + (`#12516 <https://github.com/coq/coq/pull/12516>`_, + by Maxime Dénès). +- **Added:** + The :attr:`export` locality can now be used for all Hint commands, + including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / + :cmd:`Opaque <Hint Opaque>` and + :cmd:`Remove Hints` + (`#13388 <https://github.com/coq/coq/pull/13388>`_, + by Pierre-Marie Pédrot). +- **Added:** + Support for automatic insertion of coercions in :cmd:`Search` + patterns. Additionally, head patterns are now automatically + interpreted as types + (`#13255 <https://github.com/coq/coq/pull/13255>`_, + fixes `#13244 <https://github.com/coq/coq/issues/13244>`_, + by Hugo Herbelin). +- **Added:** + The :cmd:`Proof using` command can now be used without loading the + Ltac plugin (`-noinit` mode) + (`#13339 <https://github.com/coq/coq/pull/13339>`_, + by Théo Zimmermann). +- **Added:** + Clarify in the documentation that :cmd:`Add ML Path` is not exported to compiled files + (`#13345 <https://github.com/coq/coq/pull/13345>`_, + fixes `#13344 <https://github.com/coq/coq/issues/13344>`_, + by Hugo Herbelin). + +Tools +^^^^^ + +- **Changed:** + Option `-native-compiler` of the configure script now impacts the + default value of the `-native-compiler` option of coqc. The + `-native-compiler` option of the configure script supports a new `ondemand` + value, which becomes the default, thus preserving the previous default + behavior. + The stdlib is still precompiled when configuring with `-native-compiler + yes`. It is not precompiled otherwise. + This an implementation of point 2 of + `CEP #48 <https://github.com/coq/ceps/pull/48>`_ + (`#13352 <https://github.com/coq/coq/pull/13352>`_, + by Pierre Roux). +- **Changed:** + Added the ability for coq_makefile to directly set the installation folders, + through the `COQLIBINSTALL` and `COQDOCINSTALL` variables. + See :ref:`coqmakefilelocal`. + (`#12389 <https://github.com/coq/coq/pull/12389>`_, by Martin Bodin, review of Enrico Tassi). +- **Removed:** The option ``-I`` of coqchk was removed (it was + deprecated in Coq 8.8) (`#12613 + <https://github.com/coq/coq/pull/12613>`_, by Gaëtan Gilbert). +- **Fixed:** + ``coqchk`` no longer reports names from inner modules of opaque modules as + axioms (`#12862 <https://github.com/coq/coq/pull/12862>`_, fixes `#12845 + <https://github.com/coq/coq/issues/12845>`_, by Jason Gross). + +CoqIDE +^^^^^^ + +- **Added:** + Support showing diffs for :cmd:`Show Proof` in CoqIDE from the :n:`View` menu. + See :ref:`showing_proof_diffs`. + (`#12874 <https://github.com/coq/coq/pull/12874>`_, + by Jim Fehrle and Enrico Tassi) +- **Added:** + Support for flag :flag:`Printing Goal Names` in View menu + (`#13145 <https://github.com/coq/coq/pull/13145>`_, + by Hugo Herbelin). + +Standard library +^^^^^^^^^^^^^^^^ + +- **Changed:** + In the reals theory changed the epsilon in the definition of the modulus of convergence for CReal from 1/n (n in positive) to 2^z (z in Z) + so that a precision coarser than one is possible. Also added an upper bound to CReal to enable more efficient computations. + (`#12186 <https://github.com/coq/coq/pull/12186>`_, + by Michael Soegtrop). +- **Changed:** + Int63 notations now match up with the rest of the standard library: :g:`a \% + m`, :g:`m == n`, :g:`m < n`, :g:`m <= n`, and :g:`m ≤ n` have been replaced + with :g:`a mod m`, :g:`m =? n`, :g:`m <? n`, :g:`m <=? n`, and :g:`m ≤? n`. + The old notations are still available as deprecated notations. Additionally, + there is now a ``Coq.Numbers.Cyclic.Int63.Int63.Int63Notations`` module that + users can import to get the ``Int63`` notations without unqualifying the + various primitives (`#12479 <https://github.com/coq/coq/pull/12479>`_, fixes + `#12454 <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). +- **Changed:** + PrimFloat notations now match up with the rest of the standard library: :g:`m + == n`, :g:`m < n`, and :g:`m <= n` have been replaced with :g:`m =? n`, :g:`m + <? n`, and :g:`m <=? n`. The old notations are still available as deprecated + notations. Additionally, there is now a + ``Coq.Floats.PrimFloat.PrimFloatNotations`` module that users can import to + get the ``PrimFloat`` notations without unqualifying the various primitives + (`#12556 <https://github.com/coq/coq/pull/12556>`_, fixes `#12454 + <https://github.com/coq/coq/issues/12454>`_, by Jason Gross). +- **Changed:** the sort of cyclic numbers from Type to Set. + For backward compatibility, a dynamic sort was defined in the 3 packages bignums, coqprime and color. + See for example commit 6f62bda in bignums. + (`#12801 <https://github.com/coq/coq/pull/12801>`_, + by Vincent Semeria). +- **Changed:** + ``Require Import Coq.nsatz.NsatzTactic`` now allows using :tacn:`nsatz` + with `Z` and `Q` without having to supply instances or using ``Require Import Coq.nsatz.Nsatz``, which + transitively requires unneeded files declaring axioms used in the reals + (`#12861 <https://github.com/coq/coq/pull/12861>`_, + fixes `#12860 <https://github.com/coq/coq/issues/12860>`_, + by Jason Gross). +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#12716 <https://github.com/coq/coq/pull/12716>`_, + by Yishuai Li). +- **Added:** + New lemmas about ``repeat`` in ``List`` and ``Permutation``: ``repeat_app``, ``repeat_eq_app``, ``repeat_eq_cons``, ``repeat_eq_elt``, ``Forall_eq_repeat``, ``Permutation_repeat`` + (`#12799 <https://github.com/coq/coq/pull/12799>`_, + by Olivier Laurent). +- **Added:** + Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. + (`#12094 <https://github.com/coq/coq/pull/12094>`_, + fixes `#12093 <https://github.com/coq/coq/issues/12093>`_, + by Edward Wang). +- **Added:** + ``Decidable`` instance for negation + (`#12420 <https://github.com/coq/coq/pull/12420>`_, + by Yishuai Li). +- **Fixed:** + `Coq.Program.Wf.Fix_F_inv` and `Coq.Program.Wf.Fix_eq` are now axiom-free. They no longer assume proof irrelevance. + (`#13365 <https://github.com/coq/coq/pull/13365>`_, + by Li-yao Xia). + +Infrastructure and dependencies +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + When compiled with OCaml >= 4.10.0, Coq will use the new best-fit GC + policy, which should provide some performance benefits. Coq's policy + is optimized for speed, but could increase memory consumption in + some cases. You are welcome to tune it using the ``OCAMLRUNPARAM`` + variable and report back on good settings so we can improve the defaults. + (`#13040 <https://github.com/coq/coq/pull/13040>`_, + fixes `#11277 <https://github.com/coq/coq/issues/11277>`_, + by Emilio Jesus Gallego Arias). +- **Changed:** + Coq now uses the `zarith <https://github.com/ocaml/Zarith>`_ + library, based on GNU's gmp instead of ``num`` which is + deprecated upstream. The custom ``bigint`` module is + no longer provided. + (`#11742 <https://github.com/coq/coq/pull/11742>`_, + `#13007 <https://github.com/coq/coq/pull/13007>`_, + by Emilio Jesus Gallego Arias and Vicent Laporte, with help from + Frédéric Besson). + Version 8.12 ------------ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index df73de846f..64deb692fd 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -588,6 +588,8 @@ As an exception, if the right-hand side is just of the form :n:`@@qualid`, this conventionally stops the inheritance of implicit arguments (but not of notation scopes). +.. _notations-and-binders: + Notations and binders ~~~~~~~~~~~~~~~~~~~~~ |