diff options
138 files changed, 1317 insertions, 804 deletions
diff --git a/coq-doc.opam b/coq-doc.opam index 67cdbd8bf0..3a872db33d 100644 --- a/coq-doc.opam +++ b/coq-doc.opam @@ -20,7 +20,8 @@ depends: [ "coq" {build & = version} ] build: [ - ["dune" "subst"] {pinned} +# Disabled until Dune 2.8 is available +# ["dune" "subst"] {pinned} [ "dune" "build" @@ -26,7 +26,8 @@ depends: [ "zarith" {>= "1.10"} ] build: [ - ["dune" "subst"] {pinned} +# Disabled until Dune 2.8 is available +# ["dune" "subst"] {pinned} [ "dune" "build" diff --git a/coq.opam.docker b/coq.opam.docker index 74ca68ac0b..253e648d3e 100644 --- a/coq.opam.docker +++ b/coq.opam.docker @@ -27,8 +27,14 @@ depends: [ "conf-findutils" {build} ] +depopts: [ + "coq-native" +] + build: [ - [ "./configure" "-prefix" prefix "-coqide" "no" ] + [ "./configure" "-prefix" prefix "-coqide" "no" + "-native-compiler" "yes" {coq-native:installed} "no" {!coq-native:installed} + ] [make "-j%{jobs}%"] [make "-j%{jobs}%" "byte"] ] diff --git a/coqide-server.opam b/coqide-server.opam index 101cd4ad78..cbb0db2893 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -23,7 +23,8 @@ depends: [ "coq" {= version} ] build: [ - ["dune" "subst"] {pinned} +# Disabled until Dune 2.8 is available +# ["dune" "subst"] {pinned} [ "dune" "build" diff --git a/coqide.opam b/coqide.opam index 3007200fe5..9e4fb05701 100644 --- a/coqide.opam +++ b/coqide.opam @@ -21,7 +21,8 @@ depends: [ "coqide-server" {= version} ] build: [ - ["dune" "subst"] {pinned} +# Disabled until Dune 2.8 is available +# ["dune" "subst"] {pinned} [ "dune" "build" diff --git a/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh b/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh new file mode 100644 index 0000000000..aa686ea619 --- /dev/null +++ b/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "13537" ] || [ "$CI_BRANCH" = "lazy-subst-kernel" ]; then + + overlay mtac2 https://github.com/ppedrot/Mtac2 lazy-subst-kernel + +fi diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 9b43bddd86..39ad7f3b8f 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -117,15 +117,14 @@ in time. Coq has been tagged. - [ ] Have some people test the recently auto-generated Windows and MacOS packages. -- [ ] In a PR: +- [ ] In a PR against `vX.X` (for testing): - Change the version name from alpha to beta1 (see [#7009](https://github.com/coq/coq/pull/7009/files)). - We generally do not update the magic numbers at this point. - Set `is_a_released_version` to `true` in `configure.ml`. - [ ] Put the `VX.X+beta1` tag using `git tag -s`. -- [ ] Check using `git push --tags --dry-run` that you are not - pushing anything else than the new tag. If needed, remove spurious - tags with `git tag -d`. When this is OK, proceed with `git push --tags`. +- [ ] Push the new tag with `git push upstream VX.X+beta1 --dry-run` + (remove the `--dry-run` and redo if all looks OK). - [ ] Set `is_a_released_version` to `false` in `configure.ml` (if you forget about it, you'll be reminded whenever you try to backport a PR with a changelog entry). @@ -141,29 +140,28 @@ in time. - [ ] Draft a release on GitHub. - [ ] Sign the Windows and MacOS packages and upload them on GitHub. + The Windows packages must be signed by the Inria IT security service. They - should be sent as a link to the binary together with its SHA256 hash in a - signed e-mail, via our local contact (currently `@maximedenes`). - + The MacOS packages should be signed by our own certificate, by sending them - to `@maximedenes`. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases). + should be sent as a link to the binary (via [filesender](https://filesender.renater.fr) for example) + together with its SHA256 hash in a signed e-mail to `dsi.securite` @ `inria.fr` + putting `@maximedenes` in carbon copy. + + The MacOS packages should be signed with our own certificate. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases). - [ ] Prepare a page of news on the website with the link to the GitHub release (see [coq/www#63](https://github.com/coq/www/pull/63)). -- [ ] Upload the new version of the reference manual to the website. - *TODO: setup some continuous deployment for this.* - [ ] Merge the website update, publish the release - and send announcement e-mails. + and send announcement e-mails, typically on + the `coq-club@inria.fr` mailing list and the discourse forum + ([posting by mail](https://github.com/coq/coq/wiki/Discourse)) - [ ] Close the milestone ## At the final release time ## - [ ] Prepare the release notes (see above) -- [ ] In a PR: +- [ ] In a PR against `vX.X` (for testing): - Change the version name from X.X.0 and the magic numbers (see [#7271](https://github.com/coq/coq/pull/7271/files)). - Set `is_a_released_version` to `true` in `configure.ml`. - [ ] Put the `VX.X.0` tag. -- [ ] Check using `git push --tags --dry-run` that you are not - pushing anything else than the new tag. If needed, remove spurious - tags with `git tag -d`. When this is OK, proceed with `git push --tags`. +- [ ] Push the new tag with `git push upstream VX.X.0 --dry-run` + (remove the `--dry-run` and redo if all looks OK). - [ ] Set `is_a_released_version` to `false` in `configure.ml` (if you forget about it, you'll be reminded whenever you try to backport a PR with a changelog entry). 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/01-kernel/13501-fix-13495.rst b/doc/changelog/01-kernel/13501-fix-13495.rst deleted file mode 100644 index 5c81efa8b9..0000000000 --- a/doc/changelog/01-kernel/13501-fix-13495.rst +++ /dev/null @@ -1,7 +0,0 @@ -- **Fixed:** - Fix an incompleteness in the typechecking of `match` for - cumulative inductive types. This could result in breaking subject - reduction. - (`#13501 <https://github.com/coq/coq/pull/13501>`_, - fixes `#13495 <https://github.com/coq/coq/issues/13495>`_, - by Matthieu Sozeau). 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/05-tactic-language/13442-ltac2-abstract-ffi.rst b/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst new file mode 100644 index 0000000000..26b72de2aa --- /dev/null +++ b/doc/changelog/05-tactic-language/13442-ltac2-abstract-ffi.rst @@ -0,0 +1,6 @@ +- **Added:** + A function Ltac1.lambda allowing to embed Ltac2 functions + into Ltac1 runtime values + (`#13442 <https://github.com/coq/coq/pull/13442>`_, + fixes `#12871 <https://github.com/coq/coq/issues/12871>`_, + 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/07-commands-and-options/13556-master.rst b/doc/changelog/07-commands-and-options/13556-master.rst new file mode 100644 index 0000000000..05a60026a3 --- /dev/null +++ b/doc/changelog/07-commands-and-options/13556-master.rst @@ -0,0 +1,4 @@ +- **Changed:** + The warning `custom-entry-overriden` has been renamed to `custom-entry-overridden` (with two d's). + (`#13556 <https://github.com/coq/coq/pull/13556>`_, + by Simon Friis Vindum). 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..8fb03879e8 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -8,6 +8,687 @@ 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). + +- **Fixed:** + Fix an incompleteness in the typechecking of `match` for + cumulative inductive types. This could result in breaking subject + reduction. + (`#13501 <https://github.com/coq/coq/pull/13501>`_, + fixes `#13495 <https://github.com/coq/coq/issues/13495>`_, + by Matthieu Sozeau). + +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/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index 95c5914e47..d178311b4c 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -79,7 +79,7 @@ Setting properties of a function's arguments `!` the function will be unfolded only if all the arguments marked with `!` - evaulate to constructors. See :ref:`Args_effect_on_unfolding`. + evaluate to constructors. See :ref:`Args_effect_on_unfolding`. :n:`@name {? % @scope }` a *formal parameter* of the function :n:`@reference` (i.e. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index df73de846f..73f90b0056 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -309,7 +309,7 @@ at the time of use of the notation. a notation should only be used for printing. If a notation to be used both for parsing and printing is - overriden, both the parsing and printing are invalided, even if the + overridden, both the parsing and printing are invalided, even if the overriding rule is only parsing. If a given notation string occurs only in ``only printing`` rules, @@ -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 ~~~~~~~~~~~~~~~~~~~~~ @@ -1707,6 +1709,8 @@ Number notations * :n:`Number.uint -> option @qualid__type` * :n:`Z -> @qualid__type` * :n:`Z -> option @qualid__type` + * :n:`Int63.int -> @qualid__type` + * :n:`Int63.int -> option @qualid__type` * :n:`Number.number -> @qualid__type` * :n:`Number.number -> option @qualid__type` @@ -1719,6 +1723,8 @@ Number notations * :n:`@qualid__type -> option Number.uint` * :n:`@qualid__type -> Z` * :n:`@qualid__type -> option Z` + * :n:`@qualid__type -> Int63.int` + * :n:`@qualid__type -> option Int63.int` * :n:`@qualid__type -> Number.number` * :n:`@qualid__type -> option Number.number` @@ -1823,6 +1829,13 @@ Number notations only for integers or non-negative integers, and the given number has a fractional or exponent part or is negative. + .. exn:: int63 are only non-negative numbers. + + :n:`Int63.int` are unsigned integers. + + .. exn:: overflow in int63 literal @bigint + + The constant is too big to fit into an unsigned 63-bit integer :n:`Int63.int`. .. exn:: @qualid__parse should go from Number.int to @type or (option @type). Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first). diff --git a/dune-project b/dune-project index 1265c993b7..1187c58449 100644 --- a/dune-project +++ b/dune-project @@ -5,7 +5,10 @@ (formatting (enabled_for ocaml)) -(generate_opam_files true) +; Pending on dune 2.8 as to avoid bug with dune subst +; see https://github.com/ocaml/dune/pull/3879 and +; https://github.com/ocaml/dune/pull/3879 +; (generate_opam_files true) (license LGPL-2.1-only) (maintainers "The Coq development team <coqdev@inria.fr>") diff --git a/engine/uState.ml b/engine/uState.ml index 0c994dfea0..20ea24dd87 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -113,19 +113,18 @@ let constraints uctx = snd uctx.local let context uctx = ContextSet.to_context uctx.local let compute_instance_binders inst ubinders = - let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in let map lvl = - try Name (LMap.find lvl revmap) - with Not_found -> Anonymous + try Name (Option.get (LMap.find lvl ubinders).uname) + with Option.IsNone | Not_found -> Anonymous in Array.map map (Instance.to_array inst) let univ_entry ~poly uctx = let open Entries in if poly then - let (binders, _) = uctx.names in + let (_, rbinders) = uctx.names in let uctx = context uctx in - let nas = compute_instance_binders (UContext.instance uctx) binders in + let nas = compute_instance_binders (UContext.instance uctx) rbinders in Polymorphic_entry (nas, uctx) else Monomorphic_entry (context_set uctx) @@ -158,23 +157,8 @@ let of_binders names = in { empty with names = (names, rev_map) } -let invent_name (named,cnt) u = - let rec aux i = - let na = Id.of_string ("u"^(string_of_int i)) in - if Id.Map.mem na named then aux (i+1) - else Id.Map.add na u named, i+1 - in - aux cnt - let universe_binders uctx = - let named, rev = uctx.names in - let named, _ = LSet.fold (fun u named -> - match LMap.find u rev with - | exception Not_found -> (* not sure if possible *) invent_name named u - | { uname = None } -> invent_name named u - | { uname = Some _ } -> named) - (ContextSet.levels uctx.local) (named, 0) - in + let named, _ = uctx.names in named let instantiate_variable l b v = @@ -447,9 +431,9 @@ let check_univ_decl ~poly uctx decl = let names = decl.univdecl_instance in let extensible = decl.univdecl_extensible_instance in if poly then - let (binders, _) = uctx.names in + let (_, rbinders) = uctx.names in let uctx = universe_context ~names ~extensible uctx in - let nas = compute_instance_binders (UContext.instance uctx) binders in + let nas = compute_instance_binders (UContext.instance uctx) rbinders in Entries.Polymorphic_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in diff --git a/engine/uState.mli b/engine/uState.mli index 442c29180c..9cff988c99 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -79,7 +79,7 @@ val univ_entry : poly:bool -> t -> Entries.universes_entry (** Pick from {!context} or {!context_set} based on [poly]. *) val universe_binders : t -> UnivNames.universe_binders -(** Return names of universes, inventing names if needed *) +(** Return local names of universes. *) (** {5 Constraints handling} *) diff --git a/engine/univNames.ml b/engine/univNames.ml index f5542cc0f7..215f27f535 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -15,7 +15,7 @@ open Univ let qualid_of_level ctx l = match Level.name l with | Some qid -> - (try Some (Nametab.shortest_qualid_of_universe (Id.Map.domain ctx) qid) + (try Some (Nametab.shortest_qualid_of_universe ctx qid) with Not_found -> None) | None -> None diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c9326615dc..d2256720c4 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -759,6 +759,10 @@ let get_nth_arg head n stk = | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as s -> (None, List.rev rstk @ s) in strip_rec [] head n stk +let rec subs_consn v i n s = + if Int.equal i n then s + else subs_consn v (i + 1) n (subs_cons v.(i) s) + (* Beta reduction: look for an applied argument in the stack. Since the encountered update marks are removed, h must be a whnf *) let rec get_args n tys f e = function @@ -770,14 +774,13 @@ let rec get_args n tys f e = function get_args n tys f (subs_shft (k,e)) s | Zapp l :: s -> let na = Array.length l in - if n == na then (Inl (subs_cons(l,e)),s) + if n == na then (Inl (subs_consn l 0 na e), s) else if n < na then (* more arguments *) - let args = Array.sub l 0 n in let eargs = Array.sub l n (na-n) in - (Inl (subs_cons(args,e)), Zapp eargs :: s) + (Inl (subs_consn l 0 n e), Zapp eargs :: s) else (* more lambdas *) let etys = List.skipn na tys in - get_args (n-na) etys f (subs_cons(l,e)) s + get_args (n-na) etys f (subs_consn l 0 na e) s | ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk -> (Inr {mark=mark Cstr Unknown;term=FLambda(n,tys,f,e)}, stk) @@ -931,7 +934,11 @@ let contract_fix_vect fix = env, Array.length bds) | _ -> assert false in - (subs_cons(Array.init nfix make_body, env), thisbody) + let rec mk_subs env i = + if Int.equal i nfix then env + else mk_subs (subs_cons (make_body i) env) (i + 1) + in + (mk_subs env 0, thisbody) let unfold_projection info p = if red_projection info.i_flags p @@ -1367,7 +1374,7 @@ let rec knr info tab m stk = knit info tab fxe fxbd (args@stk') | (_,args, ((Zapp _ | Zfix _ | Zshift _ | Zupdate _ | Zprimitive _) :: _ | [] as s)) -> (m,args@s)) | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> - knit info tab (subs_cons([|v|],e)) bd stk + knit info tab (subs_cons v e) bd stk | FEvar(ev,env) -> (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk @@ -1417,7 +1424,7 @@ and case_inversion info tab ci (univs,args) v = let env = info_env info in let ind = ci.ci_ind in let params, indices = Array.chop ci.ci_npar args in - let psubst = subs_cons (params, subs_id 0) in + let psubst = subs_consn params 0 ci.ci_npar (subs_id 0) in let mib = Environ.lookup_mind (fst ind) env in let mip = mib.mind_packets.(snd ind) in (* indtyping enforces 1 ctor with no letins in the context *) diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 3e8502b988..afd8e3ef67 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -60,127 +60,188 @@ let rec is_lift_id = function (* Substitutions *) (*********************) -(* (bounded) explicit substitutions of type 'a *) -type 'a subs = - | ESID of int (* ESID(n) = %n END bounded identity *) - | CONS of 'a array * 'a subs - (* CONS([|t1..tn|],S) = - (S.t1...tn) parallel substitution - beware of the order *) - | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *) - (* with n vars *) - | LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *) - -(* operations of subs: collapses constructors when possible. - * Needn't be recursive if we always use these functions - *) - -let subs_id i = ESID i - -let subs_cons(x,s) = if Int.equal (Array.length x) 0 then s else CONS(x,s) - -let subs_liftn n = function - | ESID p -> ESID (p+n) (* bounded identity lifted extends by p *) - | LIFT (p,lenv) -> LIFT (p+n, lenv) - | lenv -> LIFT (n,lenv) - -let subs_lift a = subs_liftn 1 a -let subs_liftn n a = if Int.equal n 0 then a else subs_liftn n a - -let subs_shft = function - | (0, s) -> s - | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1) - | (n, s) -> SHIFT (n,s) -let subs_shft s = if Int.equal (fst s) 0 then snd s else subs_shft s - -let subs_shift_cons = function - (0, s, t) -> CONS(t,s) -| (k, SHIFT(n,s1), t) -> CONS(t,SHIFT(k+n, s1)) -| (k, s, t) -> CONS(t,SHIFT(k, s));; - -(* Tests whether a substitution is equal to the identity *) -let rec is_subs_id = function - ESID _ -> true - | LIFT(_,s) -> is_subs_id s - | SHIFT(0,s) -> is_subs_id s - | CONS(x,s) -> Int.equal (Array.length x) 0 && is_subs_id s - | _ -> false - -(* Expands de Bruijn k in the explicit substitution subs - * lams accumulates de shifts to perform when retrieving the i-th value - * the rules used are the following: - * - * [id]k --> k - * [S.t]1 --> t - * [S.t]k --> [S](k-1) if k > 1 - * [^n o S] k --> [^n]([S]k) - * [(%n S)] k --> k if k <= n - * [(%n S)] k --> [^n]([S](k-n)) - * - * the result is (Inr (k+lams,p)) when the variable is just relocated - * where p is None if the variable points inside subs and Some(k) if the - * variable points k bindings beyond subs. - *) -let rec exp_rel lams k subs = - match subs with - | CONS (def,_) when k <= Array.length def - -> Inl(lams,def.(Array.length def - k)) - | CONS (v,l) -> exp_rel lams (k - Array.length v) l - | LIFT (n,_) when k<=n -> Inr(lams+k,None) - | LIFT (n,l) -> exp_rel (n+lams) (k-n) l - | SHIFT (n,s) -> exp_rel (n+lams) k s - | ESID n when k<=n -> Inr(lams+k,None) - | ESID n -> Inr(lams+k,Some (k-n)) - -let expand_rel k subs = exp_rel 0 k subs - -let rec subs_map f = function -| ESID _ as s -> s -| CONS (x, s) -> CONS (Array.map f x, subs_map f s) -| SHIFT (n, s) -> SHIFT (n, subs_map f s) -| LIFT (n, s) -> LIFT (n, subs_map f s) - -let rec lift_subst mk_cl s1 s2 = match s1 with -| ELID -> subs_map (fun c -> mk_cl ELID c) s2 -| ELSHFT(s, k) -> subs_shft(k, lift_subst mk_cl s s2) -| ELLFT (k, s) -> - match s2 with - | CONS(x,s') -> - CONS(CArray.Fun1.map mk_cl s1 x, lift_subst mk_cl s1 s') - | ESID n -> lift_subst mk_cl s (ESID (n + k)) - | SHIFT(k',s') -> - if k<k' - then subs_shft(k, lift_subst mk_cl s (subs_shft(k'-k, s'))) - else subs_shft(k', lift_subst mk_cl (el_liftn (k-k') s) s') - | LIFT(k',s') -> - if k<k' - then subs_liftn k (lift_subst mk_cl s (subs_liftn (k'-k) s')) - else subs_liftn k' (lift_subst mk_cl (el_liftn (k-k') s) s') - -let rec comp mk_cl s1 s2 = - match (s1, s2) with - | _, ESID _ -> s1 - | ESID _, _ -> s2 - | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2) - | _, CONS(x,s') -> - CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s') - | CONS(x,s), SHIFT(k,s') -> - let lg = Array.length x in - if k == lg then comp mk_cl s s' - else if k > lg then comp mk_cl s (SHIFT(k-lg, s')) - else comp mk_cl (CONS(Array.sub x 0 (lg-k), s)) s' - | CONS(x,s), LIFT(k,s') -> - let lg = Array.length x in - if k == lg then CONS(x, comp mk_cl s s') - else if k > lg then CONS(x, comp mk_cl s (LIFT(k-lg, s'))) - else - CONS(Array.sub x (lg-k) k, - comp mk_cl (CONS(Array.sub x 0 (lg-k),s)) s') - | LIFT(k,s), SHIFT(k',s') -> - if k<k' - then subs_shft(k, comp mk_cl s (subs_shft(k'-k, s'))) - else subs_shft(k', comp mk_cl (subs_liftn (k-k') s) s') - | LIFT(k,s), LIFT(k',s') -> - if k<k' - then subs_liftn k (comp mk_cl s (subs_liftn (k'-k) s')) - else subs_liftn k' (comp mk_cl (subs_liftn (k-k') s) s') +(* Variant of skewed lists enriched w.r.t. a monoid. See the Range module. + + In addition to the indexed data, every node contains a monoid element, in our + case, integers. It corresponds to the number of partial shifts to apply when + reaching this subtree. The total shift is obtained by summing all the partial + shifts encountered in the tree traversal. For efficiency, we also cache the + sum of partial shifts of the whole subtree as the last argument of the [Node] + constructor. + + A more intuitive but inefficient representation of this data structure would + be a list of terms interspeded with shifts, as in + + type 'a subst = NIL | CONS of 'a or_var * 'a subst | SHIFT of 'a subst + + On this inefficient representation, the typing rules would be: + + · ⊢ NIL : · + Γ ⊢ σ : Δ and Γ ⊢ t : A{σ} implies Γ ⊢ CONS (t, σ) : Δ, A + Γ ⊢ σ : Δ implies Γ, A ⊢ SHIFT σ : Δ + + The efficient representation is isomorphic to this naive variant, except that + shifts are grouped together, and we use skewed lists instead of lists. + +*) + +type shf = int +let cmp n m = n + m +let idn = 0 + +type 'a or_var = Arg of 'a | Var of int + +type 'a tree = +| Leaf of shf * 'a or_var +| Node of shf * 'a or_var * 'a tree * 'a tree * shf +(* + Invariants: + - All trees are complete. + - Define get_shift inductively as [get_shift (Leaf (w, _)) := w] and + [get_shift (Node (w, _, t1, t2, _)) := w + t1 + t2] then for every tree + of the form Node (_, _, t1, t2, sub), we must have + sub = get_shift t1 + get_shift t2. + + In the naive semantics: + + Leaf (w, x) := SHIFT^w (CONS (x, NIL)) + Node (w, x, t1, t2, _) := SHIFT^w (CONS (x, t1 @ t2)) + +*) + +type 'a subs = Nil of shf * int | Cons of int * 'a tree * 'a subs +(* + In the naive semantics mentioned above, we have the following. + + Nil (w, n) stands for SHIFT^w (ID n) where ID n is a compact form of identity + substitution, defined inductively as + + ID 0 := NIL + ID (S n) := CONS (Var 1, SHIFT (ID n)) + + Cons (h, t, s) stands for (t @ s) and h is the total number of values in the + tree t. In particular, it is always of the form 2^n - 1 for some n. +*) + +(* Returns the number of shifts contained in the whole tree. *) +let eval = function +| Leaf (w, _) -> w +| Node (w1, _, _, _, w2) -> cmp w1 w2 + +let leaf x = Leaf (idn, x) +let node x t1 t2 = Node (idn, x, t1, t2, cmp (eval t1) (eval t2)) + +let rec tree_get h w t i = match t with +| Leaf (w', x) -> + let w = cmp w w' in + if i = 0 then w, Inl x else assert false +| Node (w', x, t1, t2, _) -> + let w = cmp w w' in + if i = 0 then w, Inl x + else + let h = h / 2 in + if i <= h then tree_get h w t1 (i - 1) + else tree_get h (cmp w (eval t1)) t2 (i - h - 1) + +let rec get w l i = match l with +| Nil (w', n) -> + let w = cmp w w' in + if i < n then w, Inl (Var (i + 1)) + else n + w, Inr (i - n) (* FIXME: double check *) +| Cons (h, t, rem) -> + if i < h then tree_get h w t i else get (cmp (eval t) w) rem (i - h) + +let get l i = get idn l i + +let tree_write w = function +| Leaf (w', x) -> Leaf (cmp w w', x) +| Node (w', x, t1, t2, wt) -> Node (cmp w w', x, t1, t2, wt) + +let write w l = match l with +| Nil (w', n) -> Nil (cmp w w', n) +| Cons (h, t, rem) -> Cons (h, tree_write w t, rem) + +let cons x l = match l with +| Cons (h1, t1, Cons (h2, t2, rem)) -> + if Int.equal h1 h2 then Cons (1 + h1 + h2, node x t1 t2, rem) + else Cons (1, leaf x, l) +| _ -> Cons (1, leaf x, l) + +let expand_rel n s = + let k, v = get s (n - 1) in + match v with + | Inl (Arg v) -> Inl (k, v) + | Inl (Var i) -> Inr (k + i, None) + | Inr i -> Inr (k + i + 1, Some (i + 1)) + +let is_subs_id = function +| Nil (w, _) -> Int.equal w 0 +| Cons (_, _, _) -> false + +let subs_cons v s = cons (Arg v) s + +let rec push_vars i s = + if Int.equal i 0 then s + else push_vars (pred i) (cons (Var i) s) + +let subs_liftn n s = + if Int.equal n 0 then s + else match s with + | Nil (0, m) -> Nil (0, m + n) (* Preserve identity substitutions *) + | Nil _ | Cons _ -> + let s = write n s in + push_vars n s + +let subs_lift s = match s with +| Nil (0, m) -> Nil (0, m + 1) (* Preserve identity substitutions *) +| Nil _ | Cons _ -> + cons (Var 1) (write 1 s) + +let subs_id n = Nil (0, n) + +let subs_shft (n, s) = write n s + +(* pop is the n-ary tailrec variant of a function whose typing rules would be + given as follows. Assume Γ ⊢ e : Δ, A, then + - Γ := Ξ, A, Ω for some Ξ and Ω with |Ω| := fst (pop e) + - Ξ ⊢ snd (pop e) : Δ +*) +let rec pop n i e = + if Int.equal n 0 then i, e + else match e with + | ELID -> i, e + | ELLFT (k, e) -> + if k <= n then pop (n - k) i e + else i, ELLFT (k - n, e) + | ELSHFT (e, k) -> pop n (i + k) e + +let apply mk e = function +| Var i -> Var (reloc_rel i e) +| Arg v -> Arg (mk e v) + +let rec tree_map mk e = function +| Leaf (w, x) -> + let (n, e) = pop w 0 e in + Leaf (w + n, apply mk e x), e +| Node (w, x, t1, t2, _) -> + let (n, e) = pop w 0 e in + let x = apply mk e x in + let t1, e = tree_map mk e t1 in + let t2, e = tree_map mk e t2 in + Node (w + n, x, t1, t2, cmp (eval t1) (eval t2)), e + +let rec lift_id e n = match e with +| ELID -> Nil (0, n) +| ELSHFT (e, k) -> write k (lift_id e n) +| ELLFT (k, e) -> + if k <= n then subs_liftn k (lift_id e (n - k)) + else assert false + +let rec lift_subst mk e s = match s with +| Nil (w, m) -> + let (n, e) = pop w 0 e in + write (w + n) (lift_id e m) +| Cons (h, t, rem) -> + let t, e = tree_map mk e t in + let rem = lift_subst mk e rem in + Cons (h, t, rem) diff --git a/kernel/esubst.mli b/kernel/esubst.mli index 4239e42adc..8ff29ab07a 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -11,28 +11,38 @@ (** Explicit substitutions *) (** {6 Explicit substitutions } *) -(** Explicit substitutions of type ['a]. - - ESID(n) = %n END bounded identity - - CONS([|t1..tn|],S) = (S.t1...tn) parallel substitution - (beware of the order: indice 1 is substituted by tn) - - SHIFT(n,S) = (^n o S) terms in S are relocated with n vars - - LIFT(n,S) = (%n S) stands for ((^n o S).n...1) - (corresponds to S crossing n binders) *) -type 'a subs = private - | ESID of int - | CONS of 'a array * 'a subs - | SHIFT of int * 'a subs - | LIFT of int * 'a subs +(** Explicit substitutions for some type of terms ['a]. + + Assuming terms enjoy a notion of typability Γ ⊢ t : A, where Γ is a + telescope and A a type, substitutions can be typed as Γ ⊢ σ : Δ, where + as a first approximation σ is a list of terms u₁; ...; uₙ s.t. + Δ := (x₁ : A₁), ..., (xₙ : Aₙ) and Γ ⊢ uᵢ : Aᵢ{u₁...uᵢ₋₁} for all 1 ≤ i ≤ n. + + Substitutions can be applied to terms as follows, and furthermore + if Γ ⊢ σ : Δ and Δ ⊢ t : A, then Γ ⊢ t{σ} : A{σ}. + + We make the typing rules explicit below, but we omit the explicit De Bruijn + fidgetting and leave relocations implicit in terms and types. + +*) +type 'a subs (** Derived constructors granting basic invariants *) + +(** Assuming |Γ| = n, Γ ⊢ subs_id n : Γ *) val subs_id : int -> 'a subs -val subs_cons: 'a array * 'a subs -> 'a subs + +(** Assuming Γ ⊢ σ : Δ and Γ ⊢ t : A{σ}, then Γ ⊢ subs_cons t σ : Δ, A *) +val subs_cons: 'a -> 'a subs -> 'a subs + +(** Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_shft (n, σ) : Δ *) val subs_shft: int * 'a subs -> 'a subs + +(** Unary variant of {!subst_liftn}. *) val subs_lift: 'a subs -> 'a subs -val subs_liftn: int -> 'a subs -> 'a subs -(** [subs_shift_cons(k,s,[|t1..tn|])] builds (^k s).t1..tn *) -val subs_shift_cons: int * 'a subs * 'a array -> 'a subs +(** Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_liftn n σ : Δ, Ξ *) +val subs_liftn: int -> 'a subs -> 'a subs (** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution [subs]. The result is either (Inl(lams,v)) when the variable is @@ -51,7 +61,6 @@ val is_subs_id: 'a subs -> bool mk_clos is used when a closure has to be created, i.e. when s1 is applied on an element of s2. *) -val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs (** {6 Compact representation } *) (** Compact representation of explicit relocations @@ -60,6 +69,10 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs Invariant ensured by the private flag: no lift contains two consecutive [ELSHFT] nor two consecutive [ELLFT]. + + Relocations are a particular kind of substitutions that only contain + variables. In particular, [el_*] enjoys the same typing rules as the + equivalent substitution function [subs_*]. *) type lift = private | ELID @@ -77,5 +90,7 @@ val is_lift_id : lift -> bool substitution equivalent to applying el then s. Argument mk_clos is used when a closure has to be created, i.e. when el is applied on an element of s. + + That is, if Γ ⊢ e : Δ and Δ ⊢ σ : Ξ, then Γ ⊢ lift_subst mk e σ : Ξ. *) val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 18f16f427d..b27c53ef0f 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -102,7 +102,7 @@ let decompose_Llam_Llet lam = let subst_id = subs_id 0 let lift = subs_lift let liftn = subs_liftn -let cons v subst = subs_cons([|v|], subst) +let cons v subst = subs_cons v subst let shift subst = subs_shft (1, subst) (* Linked code location utilities *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 85e24f87b7..802a32b0e7 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -198,7 +198,7 @@ let type_of_apply env func funt argsv argstv = let argt = argstv.(i) in let c1 = term_of_fconstr c1 in begin match conv_leq false env argt c1 with - | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons ([| inject arg |], e)) c2) + | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons (inject arg) e) c2) | exception NotConvertible -> error_cant_apply_bad_type env (i+1,c1,argt) diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml index 9cca204e8c..390fa58883 100644 --- a/kernel/vmlambda.ml +++ b/kernel/vmlambda.ml @@ -179,7 +179,7 @@ let decompose_Llam lam = let subst_id = subs_id 0 let lift = subs_lift let liftn = subs_liftn -let cons v subst = subs_cons([|v|], subst) +let cons v subst = subs_cons v subst let shift subst = subs_shft (1, subst) (* A generic map function *) diff --git a/library/nametab.ml b/library/nametab.ml index d5cc4f8ac5..e94b696b60 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -98,6 +98,7 @@ module type NAMETREE = sig val find : user_name -> t -> elt val exists : user_name -> t -> bool val user_name : qualid -> t -> user_name + val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> user_name -> t -> qualid val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list @@ -252,9 +253,9 @@ let exists uname tab = with Not_found -> false -let shortest_qualid ?loc ctx uname tab = +let shortest_qualid_gen ?loc hidden uname tab = let id,dir = U.repr uname in - let hidden = Id.Set.mem id ctx in + let hidden = hidden id in let rec find_uname pos dir tree = let is_empty = match pos with [] -> true | _ -> false in match tree.path with @@ -269,6 +270,9 @@ let shortest_qualid ?loc ctx uname tab = let found_dir = find_uname [] dir ptab in make_qualid ?loc (DirPath.make found_dir) id +let shortest_qualid ?loc ctx uname tab = + shortest_qualid_gen ?loc (fun id -> Id.Set.mem id ctx) uname tab + let push_node node l = match node with | Absolute (_,o) | Relative (_,o) when not (List.mem_f E.equal o l) -> o::l @@ -564,7 +568,7 @@ let shortest_qualid_of_modtype ?loc kn = let shortest_qualid_of_universe ?loc ctx kn = let sp = UnivIdMap.find kn !the_univrevtab in - UnivTab.shortest_qualid ?loc ctx sp !the_univtab + UnivTab.shortest_qualid_gen ?loc (fun id -> Id.Map.mem id ctx) sp !the_univtab let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) diff --git a/library/nametab.mli b/library/nametab.mli index fa27dcab9a..33aebca0b9 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -206,7 +206,9 @@ val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid -val shortest_qualid_of_universe : ?loc:Loc.t -> Id.Set.t -> Univ.Level.UGlobal.t -> qualid + +(** In general we have a [UnivNames.universe_binders] around rather than a [Id.Set.t] *) +val shortest_qualid_of_universe : ?loc:Loc.t -> 'u Id.Map.t -> Univ.Level.UGlobal.t -> qualid (** {5 Generic name handling} *) @@ -236,6 +238,7 @@ module type NAMETREE = sig val find : user_name -> t -> elt val exists : user_name -> t -> bool val user_name : qualid -> t -> user_name + val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> user_name -> t -> qualid val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list val match_prefixes : qualid -> t -> elt list diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 23a7b89d2c..499c9684b2 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -429,55 +429,55 @@ let cc_tactic depth additionnal_terms = match sol with None -> Tacticals.New.tclFAIL 0 (str "congruence failed") | Some reason -> - debug (fun () -> Pp.str "Goal solved, generating proof ..."); - match reason with - Discrimination (i,ipac,j,jpac) -> - let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in - let cstr=(get_constructor_info uf ipac.cnode).ci_constr in - discriminate_tac cstr p - | Incomplete -> - let open Glob_term in - let env = Proofview.Goal.env gl in - let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in - let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in - let pr_missing (c, missing) = - let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in - let holes = List.init missing (fun _ -> hole) in - Printer.pr_glob_constr_env env sigma (DAst.make @@ GApp (c, holes)) - in - let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing." - ++ fnl () ++ - str " Try " ++ - hov 8 - begin - str "\"congruence with (" ++ prlist_with_sep (fun () -> str ")" ++ spc () ++ str "(") - pr_missing terms_to_complete ++ str ")\"," - end ++ - str " replacing metavariables by arbitrary terms.") in - Tacticals.New.tclFAIL 0 msg - | Contradiction dis -> - let env = Proofview.Goal.env gl in - let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in - let ta=term uf dis.lhs and tb=term uf dis.rhs in - match dis.rule with - Goal -> proof_tac p - | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p - | HeqG id -> - let id = EConstr.of_constr id in - convert_to_goal_tac id ta tb p - | HeqnH (ida,idb) -> - let ida = EConstr.of_constr ida in - let idb = EConstr.of_constr idb in - convert_to_hyp_tac ida ta idb tb p + debug (fun () -> Pp.str "Goal solved, generating proof ..."); + match reason with + Discrimination (i,ipac,j,jpac) -> + let p=build_proof (Tacmach.New.pf_env gl) sigma uf (`Discr (i,ipac,j,jpac)) in + let cstr=(get_constructor_info uf ipac.cnode).ci_constr in + discriminate_tac cstr p + | Incomplete -> + let open Glob_term in + let env = Proofview.Goal.env gl in + let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in + let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in + let pr_missing (c, missing) = + let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in + let holes = List.init missing (fun _ -> hole) in + Printer.pr_glob_constr_env env sigma (DAst.make @@ GApp (c, holes)) + in + let msg = Pp.(str "Goal is solvable by congruence but some arguments are missing." + ++ fnl () ++ + str " Try " ++ + hov 8 + begin + str "\"congruence with (" ++ + prlist_with_sep + (fun () -> str ")" ++ spc () ++ str "(") + pr_missing terms_to_complete ++ + str ")\"," + end ++ + fnl() ++ str " replacing metavariables by arbitrary terms") + in + Tacticals.New.tclFAIL 0 msg + | Contradiction dis -> + let env = Proofview.Goal.env gl in + let p=build_proof env sigma uf (`Prove (dis.lhs,dis.rhs)) in + let ta=term uf dis.lhs and tb=term uf dis.rhs in + match dis.rule with + Goal -> proof_tac p + | Hyp id -> refute_tac (EConstr.of_constr id) ta tb p + | HeqG id -> + let id = EConstr.of_constr id in + convert_to_goal_tac id ta tb p + | HeqnH (ida,idb) -> + let ida = EConstr.of_constr ida in + let idb = EConstr.of_constr idb in + convert_to_hyp_tac ida ta idb tb p end -let cc_fail = - Tacticals.New.tclZEROMSG (Pp.str "congruence failed.") let congruence_tac depth l = - Tacticals.New.tclORELSE - (Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l)) - cc_fail + Tacticals.New.tclTHEN (Tacticals.New.tclREPEAT introf) (cc_tactic depth l) (* Beware: reflexivity = constructor 1 = apply refl_equal might be slow now, let's rather do something equivalent diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli index 52fc3acb6f..79c7d2c676 100644 --- a/plugins/cc/cctac.mli +++ b/plugins/cc/cctac.mli @@ -14,8 +14,6 @@ val proof_tac: Ccproof.proof -> unit Proofview.tactic val cc_tactic : int -> constr list -> unit Proofview.tactic -val cc_fail : unit Proofview.tactic - val congruence_tac : int -> constr list -> unit Proofview.tactic val f_equal : unit Proofview.tactic diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 2661000a39..bada2c3a60 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -111,15 +111,20 @@ let shift_value n v = * (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1})) * -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti) *) + +let rec mk_fix_subs make_body n env i = + if Int.equal i n then env + else mk_fix_subs make_body n (subs_cons (make_body i) env) (i + 1) + let contract_fixp env ((reci,i),(_,_,bds as bodies)) = let make_body j = FIXP(((reci,j),bodies), env, [||]) in let n = Array.length bds in - subs_cons(Array.init n make_body, env), bds.(i) + mk_fix_subs make_body n env 0, bds.(i) let contract_cofixp env (i,(_,_,bds as bodies)) = let make_body j = COFIXP((j,bodies), env, [||]) in let n = Array.length bds in - subs_cons(Array.init n make_body, env), bds.(i) + mk_fix_subs make_body n env 0, bds.(i) let make_constr_ref n k t = match k with @@ -401,6 +406,10 @@ let rec strip_app = function | APP (args,st) -> APP (args,strip_app st) | s -> TOP +let rec subs_consn v i n s = + if Int.equal i n then s + else subs_consn v (i + 1) n (subs_cons v.(i) s) + (* The main recursive functions * * Go under applications and cases/projections (pushed in the stack), @@ -456,7 +465,7 @@ let rec norm_head info env t stack = (* New rule: for Cbv, Delta does not apply to locally bound variables or red_set info.reds fDELTA *) - let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in + let env' = subs_cons (cbv_stack_term info TOP env b) env in norm_head info env' c stack else (CBN(t,env), stack) (* Should we consider a commutative cut ? *) @@ -526,14 +535,14 @@ and cbv_stack_value info env = function when red_set info.reds fBETA -> let nargs = Array.length args in if nargs == nlams then - cbv_stack_term info stk (subs_cons(args,env)) b + cbv_stack_term info stk (subs_consn args 0 nargs env) b else if nlams < nargs then - let env' = subs_cons(Array.sub args 0 nlams, env) in + let env' = subs_consn args 0 nlams env in let eargs = Array.sub args nlams (nargs-nlams) in cbv_stack_term info (APP(eargs,stk)) env' b else let ctxt' = List.skipn nargs ctxt in - LAM(nlams-nargs,ctxt', b, subs_cons(args,env)) + LAM(nlams-nargs,ctxt', b, subs_consn args 0 nargs env) (* a Fix applied enough -> IOTA *) | (FIXP(fix,env,[||]), stk) diff --git a/tactics/declareUctx.ml b/tactics/declareUctx.ml index bca43697cb..6c8bc92865 100644 --- a/tactics/declareUctx.ml +++ b/tactics/declareUctx.ml @@ -16,7 +16,7 @@ let name_instance inst = assert false | Some na -> try - let qid = Nametab.shortest_qualid_of_universe Names.Id.Set.empty na in + let qid = Nametab.shortest_qualid_of_universe Names.Id.Map.empty na in Names.Name (Libnames.qualid_basename qid) with Not_found -> (* Best-effort naming from the string representation of the level. diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v index 9c11d19c27..b50371386f 100644 --- a/test-suite/ltac2/compat.v +++ b/test-suite/ltac2/compat.v @@ -40,6 +40,67 @@ Fail Ltac1.run (ltac1val:(x |- idtac) 0). Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))). Abort. +(** Check value-returning FFI *) + +(* A dummy CPS wrapper in Ltac1 *) +Ltac arg k := +match goal with +| [ |- ?P ] => k P +end. + +Ltac2 testeval v := + let r := { contents := None } in + let k c := + let () := match Ltac1.to_constr c with + | None => () + | Some c => r.(contents) := Some c + end in + (* dummy return value *) + ltac1val:(idtac) + in + let tac := ltac1val:(arg) in + let () := Ltac1.apply tac [Ltac1.lambda k] (fun _ => ()) in + match r.(contents) with + | None => fail + | Some c => if Constr.equal v c then () else fail + end. + +Goal True. +Proof. +testeval 'True. +Abort. + +Goal nat. +Proof. +testeval 'nat. +Abort. + +(* CPS towers *) +Ltac2 testeval2 tac := + let fail _ := Control.zero Not_found in + let cast c := match Ltac1.to_constr c with + | None => fail () + | Some c => c + end in + let f x y z := + let x := cast x in + let y := cast y in + let z := cast z in + Ltac1.of_constr constr:($x $y $z) + in + let f := Ltac1.lambda (fun x => Ltac1.lambda (fun y => Ltac1.lambda (fun z => f x y z))) in + Ltac1.apply tac [f] Ltac1.run. + +Goal False -> True. +Proof. +ltac1:( +let ff := ltac2:(tac |- testeval2 tac) in +ff ltac:(fun k => + let c := k (fun (n : nat) (i : True) (e : False) => i) O I in + exact c) +). +Qed. + (** Test calls to Ltac2 from Ltac1 *) Set Default Proof Mode "Classic". diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 0fbb4f4c11..95b6c6ee95 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -162,6 +162,9 @@ When declaring multiple axioms in one command, only the first is allowed a unive foo@{i} = Type@{M.i} -> Type@{i} : Type@{max(M.i+1,i+1)} (* i |= *) +Type@{u0} -> Type@{UnivBinders.64} + : Type@{max(u0+1,UnivBinders.64+1)} +(* {UnivBinders.64} |= *) bind_univs.mono = Type@{bind_univs.mono.u} : Type@{bind_univs.mono.u+1} diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index ed6e90b2a6..9539e34cfe 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -161,6 +161,16 @@ Module Notas. End Notas. +Module NoAutoNames. + Monomorphic Universe u0. + + (* The anonymous universe doesn't get a name (names are only + invented at the end of a definition/inductive) so no need to + qualify u0. *) + Check (Type@{u0} -> Type). + +End NoAutoNames. + (* Universe binders survive through compilation, sections and modules. *) Require TestSuite.bind_univs. Print bind_univs.mono. diff --git a/test-suite/output/bug_12908.v b/test-suite/output/bug_12908.v index 6f7be22fa0..7ab218a27a 100644 --- a/test-suite/output/bug_12908.v +++ b/test-suite/output/bug_12908.v @@ -7,7 +7,7 @@ Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End A. Module B. -(* Test that an overriden scoped notation is deactivated *) +(* Test that an overridden scoped notation is deactivated *) Infix "*" := mult' : nat_scope. Check forall m n, mult' m n = Nat.mul (Nat.mul 2 m) n. End B. diff --git a/test-suite/output/bug_13595.out b/test-suite/output/bug_13595.out new file mode 100644 index 0000000000..2423b77b55 --- /dev/null +++ b/test-suite/output/bug_13595.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +Tactic failure: Goal is solvable by congruence but some arguments are missing. + Try "congruence with ((Triple a _ _)) ((Triple d c _))", + replacing metavariables by arbitrary terms. diff --git a/test-suite/output/bug_13595.v b/test-suite/output/bug_13595.v new file mode 100644 index 0000000000..27a9ebe15d --- /dev/null +++ b/test-suite/output/bug_13595.v @@ -0,0 +1,8 @@ +Inductive Cube:Set :=| Triple: nat -> nat -> nat -> Cube. + +Theorem incomplete :forall a b c d : nat,Triple a = Triple b->Triple d c = Triple d b->a = c. +Proof. + Fail congruence. + intros. + congruence with ((Triple a a a)) ((Triple d c a)). +Qed. diff --git a/test-suite/success/cbv_let.v b/test-suite/success/cbv_let.v new file mode 100644 index 0000000000..861a73a64e --- /dev/null +++ b/test-suite/success/cbv_let.v @@ -0,0 +1,34 @@ +Record T : Type := Build_T { f : unit; g := pair f f; }. + +Definition t : T := {| f := tt; |}. + +Goal match t return unit with Build_T f g => f end = tt. +Proof. +cbv. +reflexivity. +Qed. + +Goal match t return prod unit unit with Build_T f g => g end = pair tt tt. +Proof. +cbv. +reflexivity. +Qed. + +Goal forall (x : T), + match x return prod unit unit with Build_T f g => g end = + pair match x return unit with Build_T f g => fst g end match x return unit with Build_T f g => snd g end. +Proof. +cbv. +destruct x. +reflexivity. +Qed. + +Record U : Type := Build_U { h := tt }. + +Definition u : U := Build_U. + +Goal match u with Build_U h => h end = tt. +Proof. +cbv. +reflexivity. +Qed. diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v index 1a69708a7d..fd1555c2fb 100644 --- a/user-contrib/Ltac2/Ltac1.v +++ b/user-contrib/Ltac2/Ltac1.v @@ -25,6 +25,12 @@ Ltac2 @ external run : t -> unit := "ltac2" "ltac1_run". (** Runs an Ltac1 value, assuming it is a 'tactic', i.e. not returning anything. *) +Ltac2 @ external lambda : (t -> t) -> t := "ltac2" "ltac1_lambda". +(** Embed an Ltac2 function into Ltac1 values. Contrarily to the ltac1:(...) + quotation, this function allows both to capture an Ltac2 context inside the + closure and to return an Ltac1 value. Returning values in Ltac1 is a + intrepid endeavour prone to weird runtime semantics. *) + Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "ltac2" "ltac1_apply". (** Applies an Ltac1 value to a list of arguments, and provides the result in CPS style. It does **not** run the returned value. *) diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index 01b1025da1..8663691c0a 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1365,10 +1365,44 @@ let () = let inject (loc, v) = Ltac_plugin.Tacexpr.TacGeneric (Some "ltac2", in_gen (rawwit wit_ltac2) v) in Ltac_plugin.Tacentries.create_ltac_quotation "ltac2" inject (e, None) -(* Ltac1 runtime representation of Ltac2 closure quotations *) -let typ_ltac2 : (Id.t list * glb_tacexpr) Geninterp.Val.typ = +(* Ltac1 runtime representation of Ltac2 closures. *) +let typ_ltac2 : valexpr Geninterp.Val.typ = Geninterp.Val.create "ltac2:ltac2_eval" +let cast_typ (type a) (tag : a Geninterp.Val.typ) (v : Geninterp.Val.t) : a = + let Geninterp.Val.Dyn (tag', v) = v in + match Geninterp.Val.eq tag tag' with + | None -> assert false + | Some Refl -> v + +let () = + let open Ltac_plugin in + (* This is a hack similar to Tacentries.ml_val_tactic_extend *) + let intern_fun _ e = Empty.abort e in + let subst_fun s v = v in + let () = Genintern.register_intern0 wit_ltac2_val intern_fun in + let () = Genintern.register_subst0 wit_ltac2_val subst_fun in + (* These are bound names and not relevant *) + let tac_id = Id.of_string "F" in + let arg_id = Id.of_string "X" in + let interp_fun ist () = + let tac = cast_typ typ_ltac2 @@ Id.Map.get tac_id ist.Tacinterp.lfun in + let arg = Id.Map.get arg_id ist.Tacinterp.lfun in + let tac = Tac2ffi.to_closure tac in + Tac2ffi.apply tac [of_ltac1 arg] >>= fun ans -> + let ans = Tac2ffi.to_ext val_ltac1 ans in + Ftactic.return ans + in + let () = Geninterp.register_interp0 wit_ltac2_val interp_fun in + define1 "ltac1_lambda" valexpr begin fun f -> + let body = Tacexpr.TacGeneric (Some "ltac2", in_gen (glbwit wit_ltac2_val) ()) in + let clos = Tacexpr.TacFun ([Name arg_id], Tacexpr.TacArg (CAst.make body)) in + let f = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) f in + let lfun = Id.Map.singleton tac_id f in + let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun } in + Proofview.tclUNIT (of_ltac1 (Tacinterp.Value.of_closure ist clos)) + end + let ltac2_eval = let open Ltac_plugin in let ml_name = { @@ -1380,17 +1414,10 @@ let ltac2_eval = | tac :: args -> (* By convention the first argument is the tactic being applied, the rest being the arguments it should be fed with *) - let Geninterp.Val.Dyn (tag, tac) = tac in - let (ids, tac) : Id.t list * glb_tacexpr = match Geninterp.Val.eq tag typ_ltac2 with - | None -> assert false - | Some Refl -> tac - in - let fold accu id = match Id.Map.find id ist.Geninterp.lfun with - | v -> Id.Map.add id (Tac2ffi.of_ext val_ltac1 v) accu - | exception Not_found -> assert false - in - let env_ist = List.fold_left fold Id.Map.empty ids in - Proofview.tclIGNORE (Tac2interp.interp { env_ist } tac) + let tac = cast_typ typ_ltac2 tac in + let tac = Tac2ffi.to_closure tac in + let args = List.map (fun arg -> Tac2ffi.of_ext val_ltac1 arg) args in + Proofview.tclIGNORE (Tac2ffi.apply tac args) in let () = Tacenv.register_ml_tactic ml_name [|eval_fun|] in { Tacexpr.mltac_name = ml_name; mltac_index = 0 } @@ -1398,7 +1425,7 @@ let ltac2_eval = let () = let open Ltac_plugin in let open Tacinterp in - let interp ist (ids, tac as self) = match ids with + let interp ist (ids, tac) = match ids with | [] -> (* Evaluate the Ltac2 quotation eagerly *) let idtac = Value.of_closure { ist with lfun = Id.Map.empty } (Tacexpr.TacId []) in @@ -1413,6 +1440,8 @@ let () = let mk_arg id = Tacexpr.Reference (Locus.ArgVar (CAst.make id)) in let args = List.map mk_arg ids in let clos = Tacexpr.TacFun (nas, Tacexpr.TacML (CAst.make (ltac2_eval, mk_arg self_id :: args))) in + let self = GTacFun (List.map (fun id -> Name id) ids, tac) in + let self = Tac2interp.interp_value { env_ist = Id.Map.empty } self in let self = Geninterp.Val.inject (Geninterp.Val.Base typ_ltac2) self in let ist = { ist with lfun = Id.Map.singleton self_id self } in Ftactic.return (Value.of_closure ist clos) diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml index f6d07e484b..5479ba0d54 100644 --- a/user-contrib/Ltac2/tac2env.ml +++ b/user-contrib/Ltac2/tac2env.ml @@ -288,7 +288,8 @@ let ltac1_prefix = (** Generic arguments *) -let wit_ltac2 = Genarg.make0 "ltac2:value" +let wit_ltac2 = Genarg.make0 "ltac2:tactic" +let wit_ltac2_val = Genarg.make0 "ltac2:value" let wit_ltac2_constr = Genarg.make0 "ltac2:in-constr" let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation" let () = Geninterp.register_val0 wit_ltac2 None diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli index af1197c24c..95dcdd7e1b 100644 --- a/user-contrib/Ltac2/tac2env.mli +++ b/user-contrib/Ltac2/tac2env.mli @@ -144,6 +144,10 @@ val ltac1_prefix : ModPath.t val wit_ltac2 : (Id.t CAst.t list * raw_tacexpr, Id.t list * glb_tacexpr, Util.Empty.t) genarg_type (** Ltac2 quotations in Ltac1 code *) +val wit_ltac2_val : (Util.Empty.t, unit, Util.Empty.t) genarg_type +(** Embedding Ltac2 closures of type [Ltac1.t -> Ltac1.t] inside Ltac1. There is + no relevant data because arguments are passed by conventional names. *) + val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genarg_type (** Ltac2 quotations in Gallina terms *) diff --git a/user-contrib/Ltac2/tac2interp.ml b/user-contrib/Ltac2/tac2interp.ml index ed783afce7..8027a22e01 100644 --- a/user-contrib/Ltac2/tac2interp.ml +++ b/user-contrib/Ltac2/tac2interp.ml @@ -223,6 +223,8 @@ and eval_pure_args bnd args = let map e = eval_pure bnd None e in Array.map_of_list map args +let interp_value ist tac = + eval_pure ist.env_ist None tac (** Cross-boundary hacks. *) diff --git a/user-contrib/Ltac2/tac2interp.mli b/user-contrib/Ltac2/tac2interp.mli index e466c65224..ae7b2ea86d 100644 --- a/user-contrib/Ltac2/tac2interp.mli +++ b/user-contrib/Ltac2/tac2interp.mli @@ -18,6 +18,9 @@ val empty_environment : environment val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic +val interp_value : environment -> glb_tacexpr -> valexpr +(** Same as [interp] but assumes that the argument is a syntactic value. *) + (* val interp_app : closure -> ml_tactic *) (** {5 Cross-boundary encodings} *) diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 1987d48e0f..834ef0d29a 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -9,6 +9,8 @@ (************************************************************************) open Names +open Declarations +open Univ (* object_kind , id *) exception AlreadyDeclared of (string option * Id.t) @@ -72,23 +74,51 @@ let input_univ_names : universe_name_decl -> Libobject.obj = subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); classify_function = (fun a -> Substitute a) } +let invent_name (named,cnt) u = + let rec aux i = + let na = Id.of_string ("u"^(string_of_int i)) in + if Id.Map.mem na named then aux (i+1) + else na, (Id.Map.add na u named, i+1) + in + aux cnt + +let label_and_univs_of = let open GlobRef in function + | ConstRef c -> + let l = Label.to_id @@ Constant.label c in + let univs = (Global.lookup_constant c).const_universes in + l, univs + | IndRef (c,_) -> + let l = Label.to_id @@ MutInd.label c in + let univs = (Global.lookup_mind c).mind_universes in + l, univs + | VarRef id -> + CErrors.anomaly ~label:"declare_univ_binders" + Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") + | ConstructRef _ -> + CErrors.anomaly ~label:"declare_univ_binders" + Pp.(str "declare_univ_binders on a constructor reference") + let declare_univ_binders gr pl = - if Global.is_polymorphic gr then - () - else - let l = let open GlobRef in match gr with - | ConstRef c -> Label.to_id @@ Constant.label c - | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> - CErrors.anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") - | ConstructRef _ -> - CErrors.anomaly ~label:"declare_univ_binders" - Pp.(str "declare_univ_binders on a constructor reference") + let l, univs = label_and_univs_of gr in + match univs with + | Polymorphic _ -> () + | Monomorphic (levels,_) -> + (* First the explicitly named universes *) + let named, univs = Id.Map.fold (fun id univ (named,univs) -> + let univs = match Univ.Level.name univ with + | None -> assert false (* having Prop/Set/Var as binders is nonsense *) + | Some univ -> (id,univ)::univs + in + let named = LSet.add univ named in + named, univs) + pl (LSet.empty,[]) in - let univs = Id.Map.fold (fun id univ univs -> - match Univ.Level.name univ with - | None -> assert false (* having Prop/Set/Var as binders is nonsense *) - | Some univ -> (id,univ)::univs) pl [] + (* then invent names for the rest *) + let _, univs = LSet.fold (fun univ (aux,univs) -> + let id, aux = invent_name aux univ in + let univ = Option.get (Level.name univ) in + aux, (id,univ) :: univs) + (LSet.diff levels named) ((pl,0),univs) in Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli index ca990a58eb..a7e942be5a 100644 --- a/vernac/declareUniv.mli +++ b/vernac/declareUniv.mli @@ -10,11 +10,16 @@ open Names -(* object_kind , id *) +(** Also used by [Declare] for constants, [DeclareInd] for inductives, etc. + Containts [object_kind , id]. *) exception AlreadyDeclared of (string option * Id.t) -(** Global universe contexts, names and constraints *) +(** Internally used to declare names of universes from monomorphic + constants/inductives. Noop on polymorphic references. *) val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit +(** Command [Universes]. *) val do_universe : poly:bool -> lident list -> unit + +(** Command [Constraint]. *) val do_constraint : poly:bool -> Constrexpr.univ_constraint_expr list -> unit diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 06eb330958..e6244ee3b5 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1822,9 +1822,9 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing (* Declaration of custom entry *) let warn_custom_entry = - CWarnings.create ~name:"custom-entry-overriden" ~category:"parsing" + CWarnings.create ~name:"custom-entry-overridden" ~category:"parsing" (fun s -> - strbrk "Custom entry " ++ str s ++ strbrk " has been overriden.") + strbrk "Custom entry " ++ str s ++ strbrk " has been overridden.") let load_custom_entry _ _ = () |