From 3c4d2c9e3b7100a0012ad06b33b46fe7dca6cd29 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 30 Nov 2020 17:12:37 +0100 Subject: Changes for Coq 8.13 --- doc/changelog/01-kernel/10390-uip.rst | 5 - .../01-kernel/11604-persistent-arrays.rst | 6 - ...ster+module-starting-extends-delta-resolver.rst | 8 - doc/changelog/01-kernel/13356-primarray-cumul.rst | 5 - .../07825-rechable-from-evars.rst | 9 - .../10331-minim-prop-toset.rst | 5 - .../12653-cumul-syntax.rst | 5 - .../12756-dont-refresh-argument-names.rst | 9 - ...n-non-underscore-catch-all-pattern-matching.rst | 7 - .../13106-doc-and-changelog-for-13106.rst | 5 - ...r+fixes13165-missing-impargs-defined-fields.rst | 5 - .../02-specification-language/13183-using-att.rst | 6 - .../13188-instance-gen.rst | 6 - ...+fix13216-typeclass-for-match-return-clause.rst | 5 - ...0-master+grant13278-small-inversion-in-prop.rst | 6 - .../13312-attributes+bool_single.rst | 17 - .../13376-master+minifix-NotFoundInstance.rst | 5 - ...r+fix11816-wf-not-allowed-in-local-fixpoint.rst | 5 - ...1-primproj-canonical-structure-on-evar-type.rst | 6 - ...3387-master+fix12348-debruijn-bug-imitation.rst | 6 - ...istinguishing-ident-name-in-grammar-entries.rst | 13 - .../11986-float-low-level-printing.rst | 5 - ...erms-occurring-also-as-pattern-in-notations.rst | 4 - .../12218-numeral-notations-non-inductive.rst | 19 - ...ter+propagate-scope-in-indirect-applied-ref.rst | 6 - ...65-master+partial-app-in-recursive-notation.rst | 4 - ...zation-notations-only-parsing-only-printing.rst | 10 - ...er+fix9403-missing-flattening-app-notations.rst | 8 - ...er+fix9569-propagage-binding-vars-notations.rst | 6 - doc/changelog/03-notations/12979-doc-numbers.rst | 4 - ...84-master+import-notation-make-active-again.rst | 12 - ...12986-master+ordering-notation-by-precision.rst | 5 - ...ter+fix-13078-no-binder-in-pattern-notation.rst | 5 - .../13265-master+allow-single-binder-entry.rst | 6 - doc/changelog/03-notations/13415-intern-univs.rst | 5 - .../04-tactics/11906-micromega-booleans.rst | 4 - .../04-tactics/12246-master+apply-in-many-hyps.rst | 5 - doc/changelog/04-tactics/12399-rm-prolog.rst | 4 - doc/changelog/04-tactics/12423-rm-info.rst | 2 - doc/changelog/04-tactics/12552-zify-pre-hook.rst | 4 - doc/changelog/04-tactics/12648-zify-int63.rst | 3 - ...aster+fix13235-no-degenerate-in-hyps-clause.rst | 6 - ...ster+improve-error-dependent-intro-wildcard.rst | 6 - ...+fix13363-metas-posed-to-evars-in-wrong-env.rst | 6 - doc/changelog/04-tactics/13381-bfs_eauto.rst | 6 - doc/changelog/04-tactics/13403-occs_nums_nat.rst | 7 - doc/changelog/04-tactics/13417-no_int_or_var.rst | 7 - .../13028-master+fix-quotations-printing.rst | 6 - .../13232-ltac2-if-then-else.rst | 5 - .../06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst | 4 - .../06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst | 4 - .../12516-deprecate-grab-existentials.rst | 4 - .../13016-remove-Ocaml-value.rst | 4 - .../07-commands-and-options/13040-gc+best_fit.rst | 9 - .../13096-drop-grammar-prefixes.rst | 6 - .../13139-clean-hint-constr.rst | 6 - ...255-master+fix13244-use-coercions-in-search.rst | 7 - .../13339-proof-using-noinit.rst | 5 - .../13345-master+doc-add-ml-path-not-exported.rst | 5 - .../07-commands-and-options/13352-cep-48.rst | 12 - .../13384-warn-unqualified-hint.rst | 8 - ...13388-export-locality-for-all-hint-commands.rst | 6 - doc/changelog/08-tools/12389-coq_makefile.rst | 5 - doc/changelog/08-tools/12410-add-fixes.rst | 4 - doc/changelog/08-tools/12613-coqchk-noi.rst | 3 - doc/changelog/08-tools/12862-more-mod-checking.rst | 4 - doc/changelog/09-coqide/12874-show_proof_diffs.rst | 5 - ...5-master+coqide-printing-goal-names-support.rst | 4 - .../10-standard-library/12094-app_inj_tail.rst | 5 - .../12186-creal-new-modulus.rst | 5 - .../10-standard-library/12420-decidable.rst | 4 - .../12479-fix-int-ltb-notations.rst | 9 - .../12556-fix-float-ltb-notations.rst | 9 - doc/changelog/10-standard-library/12716-curry.rst | 4 - .../10-standard-library/12799-list-repeat.rst | 4 - .../10-standard-library/12801-cyclic-set.rst | 5 - .../12861-nsatz-tactic-instances.rst | 7 - .../10-standard-library/13365-axiom-free-wf.rst | 4 - .../11742-zarith+core.rst | 8 - .../13007-zarith+goodbye_num.rst | 4 - .../12-misc/12586-declare+typing_flags.rst | 6 - doc/sphinx/changes.rst | 661 +++++++++++++++++++++ 82 files changed, 661 insertions(+), 493 deletions(-) delete mode 100644 doc/changelog/01-kernel/10390-uip.rst delete mode 100644 doc/changelog/01-kernel/11604-persistent-arrays.rst delete mode 100644 doc/changelog/01-kernel/12537-master+module-starting-extends-delta-resolver.rst delete mode 100644 doc/changelog/01-kernel/13356-primarray-cumul.rst delete mode 100644 doc/changelog/02-specification-language/07825-rechable-from-evars.rst delete mode 100644 doc/changelog/02-specification-language/10331-minim-prop-toset.rst delete mode 100644 doc/changelog/02-specification-language/12653-cumul-syntax.rst delete mode 100644 doc/changelog/02-specification-language/12756-dont-refresh-argument-names.rst delete mode 100644 doc/changelog/02-specification-language/12768-master+warn-non-underscore-catch-all-pattern-matching.rst delete mode 100644 doc/changelog/02-specification-language/13106-doc-and-changelog-for-13106.rst delete mode 100644 doc/changelog/02-specification-language/13166-master+fixes13165-missing-impargs-defined-fields.rst delete mode 100644 doc/changelog/02-specification-language/13183-using-att.rst delete mode 100644 doc/changelog/02-specification-language/13188-instance-gen.rst delete mode 100644 doc/changelog/02-specification-language/13217-master+fix13216-typeclass-for-match-return-clause.rst delete mode 100644 doc/changelog/02-specification-language/13290-master+grant13278-small-inversion-in-prop.rst delete mode 100644 doc/changelog/02-specification-language/13312-attributes+bool_single.rst delete mode 100644 doc/changelog/02-specification-language/13376-master+minifix-NotFoundInstance.rst delete mode 100644 doc/changelog/02-specification-language/13383-master+fix11816-wf-not-allowed-in-local-fixpoint.rst delete mode 100644 doc/changelog/02-specification-language/13386-master+fix9971-primproj-canonical-structure-on-evar-type.rst delete mode 100644 doc/changelog/02-specification-language/13387-master+fix12348-debruijn-bug-imitation.rst delete mode 100644 doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst delete mode 100644 doc/changelog/03-notations/11986-float-low-level-printing.rst delete mode 100644 doc/changelog/03-notations/12099-master+constraining-terms-occurring-also-as-pattern-in-notations.rst delete mode 100644 doc/changelog/03-notations/12218-numeral-notations-non-inductive.rst delete mode 100644 doc/changelog/03-notations/12685-master+propagate-scope-in-indirect-applied-ref.rst delete mode 100644 doc/changelog/03-notations/12765-master+partial-app-in-recursive-notation.rst delete mode 100644 doc/changelog/03-notations/12950-master+reorganization-notations-only-parsing-only-printing.rst delete mode 100644 doc/changelog/03-notations/12960-master+fix9403-missing-flattening-app-notations.rst delete mode 100644 doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst delete mode 100644 doc/changelog/03-notations/12979-doc-numbers.rst delete mode 100644 doc/changelog/03-notations/12984-master+import-notation-make-active-again.rst delete mode 100644 doc/changelog/03-notations/12986-master+ordering-notation-by-precision.rst delete mode 100644 doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst delete mode 100644 doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst delete mode 100644 doc/changelog/03-notations/13415-intern-univs.rst delete mode 100644 doc/changelog/04-tactics/11906-micromega-booleans.rst delete mode 100644 doc/changelog/04-tactics/12246-master+apply-in-many-hyps.rst delete mode 100644 doc/changelog/04-tactics/12399-rm-prolog.rst delete mode 100644 doc/changelog/04-tactics/12423-rm-info.rst delete mode 100644 doc/changelog/04-tactics/12552-zify-pre-hook.rst delete mode 100644 doc/changelog/04-tactics/12648-zify-int63.rst delete mode 100644 doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst delete mode 100644 doc/changelog/04-tactics/13337-master+improve-error-dependent-intro-wildcard.rst delete mode 100644 doc/changelog/04-tactics/13373-master+fix13363-metas-posed-to-evars-in-wrong-env.rst delete mode 100644 doc/changelog/04-tactics/13381-bfs_eauto.rst delete mode 100644 doc/changelog/04-tactics/13403-occs_nums_nat.rst delete mode 100644 doc/changelog/04-tactics/13417-no_int_or_var.rst delete mode 100644 doc/changelog/05-tactic-language/13028-master+fix-quotations-printing.rst delete mode 100644 doc/changelog/05-tactic-language/13232-ltac2-if-then-else.rst delete mode 100644 doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rst delete mode 100644 doc/changelog/06-ssreflect/13459-ssr_dup_swap_apply_ipat.rst delete mode 100644 doc/changelog/07-commands-and-options/12516-deprecate-grab-existentials.rst delete mode 100644 doc/changelog/07-commands-and-options/13016-remove-Ocaml-value.rst delete mode 100644 doc/changelog/07-commands-and-options/13040-gc+best_fit.rst delete mode 100644 doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst delete mode 100644 doc/changelog/07-commands-and-options/13139-clean-hint-constr.rst delete mode 100644 doc/changelog/07-commands-and-options/13255-master+fix13244-use-coercions-in-search.rst delete mode 100644 doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst delete mode 100644 doc/changelog/07-commands-and-options/13345-master+doc-add-ml-path-not-exported.rst delete mode 100644 doc/changelog/07-commands-and-options/13352-cep-48.rst delete mode 100644 doc/changelog/07-commands-and-options/13384-warn-unqualified-hint.rst delete mode 100644 doc/changelog/07-commands-and-options/13388-export-locality-for-all-hint-commands.rst delete mode 100644 doc/changelog/08-tools/12389-coq_makefile.rst delete mode 100644 doc/changelog/08-tools/12410-add-fixes.rst delete mode 100644 doc/changelog/08-tools/12613-coqchk-noi.rst delete mode 100644 doc/changelog/08-tools/12862-more-mod-checking.rst delete mode 100644 doc/changelog/09-coqide/12874-show_proof_diffs.rst delete mode 100644 doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst delete mode 100644 doc/changelog/10-standard-library/12094-app_inj_tail.rst delete mode 100644 doc/changelog/10-standard-library/12186-creal-new-modulus.rst delete mode 100644 doc/changelog/10-standard-library/12420-decidable.rst delete mode 100644 doc/changelog/10-standard-library/12479-fix-int-ltb-notations.rst delete mode 100644 doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst delete mode 100644 doc/changelog/10-standard-library/12716-curry.rst delete mode 100644 doc/changelog/10-standard-library/12799-list-repeat.rst delete mode 100644 doc/changelog/10-standard-library/12801-cyclic-set.rst delete mode 100644 doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst delete mode 100644 doc/changelog/10-standard-library/13365-axiom-free-wf.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/11742-zarith+core.rst delete mode 100644 doc/changelog/11-infrastructure-and-dependencies/13007-zarith+goodbye_num.rst delete mode 100644 doc/changelog/12-misc/12586-declare+typing_flags.rst 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 `_, - 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 `_, - 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 `_, fixes `#12525 - `_ and `#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 - `_, fixes `#13354 - `_, by Gaëtan Gilbert). 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 `_, by Matthieu - Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and - Enrico Tassi, fixes `#4095 `_ and - `#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 - `_, by Gaëtan Gilbert with - help from Maxime Dénès and Matthieu Sozeau, fixes `#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 ` - mode) (`#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 `_, - fixes `#12001 `_ - and `#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 `_, - fixes `#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 `_, - 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 `_, - fixes `#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 `_, - 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 ` 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 `_, fixes `#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 `_, - fixes `#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 `_, - grants `#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 ` 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) `, - :attr:`universes(template=no) ` - and :attr:`universes(cumulative=no) `. - 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 `_, - 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 `_, - fixes `#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 `_, - fixes `#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 `_, - fixes `#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 `_, - fixes `#12348 `_, - by Hugo Herbelin). 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 `_, - fixes `#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 `_, - 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 `_, - 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 ` and :ref:`String Notation - ` commands now - support parameterized inductive and non inductive types - (`#12218 `_, - fixes `#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 - `_, 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 `_, - 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 `_, - fixes `#4738 `_ - and `#9682 `_ - and part 2 of `#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 `_, - fixes `#9403 `_ - and `#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 `_, - fixes `#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 ` instead. - (`#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 - `_ of a priority given to - notations which match a larger part of the term to print - (`#12984 `_, - fixes `#7443 `_ - and `#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 `_, - 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 `_, - fixes `#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 `_, - 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 `_, fixes - `#13303 `_, by Gaëtan - Gilbert). 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 `_, 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 `_, - by Hugo Herbelin; grants - `#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 `_, - 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 `_, 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 `_, - 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 `_, 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 `_, - fixes `#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 `_, - fixes `#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 `_, - fixes `#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 `_, - 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 `_, - 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 `_, - by Jim Fehrle). 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 `_, - fixes `#9716 `_ - and `#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 `_, - fixes `#10110 `_, - by Pierre-Marie Pédrot). 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 `_, - 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 `_, - by Cyril Cohen). 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 `_, - 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 `_ - (`#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 `_, - fixes `#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 `_, - 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 `_, - 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 `_, - fixes `#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 `_, - 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 `_, - fixes `#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 `_ - (`#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 `_, - 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 `_, - by Pierre-Marie Pédrot). 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 `_, 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 `_, fixes `#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 - `_, 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 `_, fixes `#12845 - `_, by Jason Gross). 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 `_, - 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 `_, - by Hugo Herbelin). 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 `_, - fixes `#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 `_, - 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 `_, - 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 `_, fixes - `#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 - `_, fixes `#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 `_, - 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 `_, - 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 `_, - 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 `_, - fixes `#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 `_, - by Li-yao Xia). 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 `_ - 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 `_, - 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 `_, - by Emilio Jesus Gallego Arias). 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 `_, - by Emilio Jesus Gallego Arias). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 249c7794be..e97fba3546 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -8,6 +8,667 @@ 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: + + - Introduction of :ref:`primitive persistent arrays` + in the core language, implemented using imperative persistent arrays. + - Introduction of definitional proof irrelevance for the equality type + defined in the SProp sort, using the :flag:`Definitional UIP` flag, + (deactivated by default). This models definitional uniqueness of + identity proofs for this type. It is deactivated by default as + it results in non-termination in combination with impredicativity. + Use of this flag is also shown by :cmd:`Print Assumptions`. + - Cumulative record and inductives 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 warning for `Hint` commands outside sections without a locality + attribute, whose goal is to eventually remove the fragile default + behavior of having hints be imported when using `Require` only. + 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 `_ + 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 improvements in :tacn:`lia` and its :tacn:`zify` preprocessing step, + now supporting reasoning on boolean operators such as `Z.leb` and supporting + primitive integers :g:`Int63`. + - Typing flags can now be specified :ref:`per-constant / inductive <813TypingFlags>`. + +See the `Changes in 8.13`_ 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 +`_ 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/. + +TODO updated maintainers +Our current 31 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, 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, 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, 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 +`_ and the `Coq Zulip chat `_. + +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 PRs merged, closing ~100 issues. + +| Nantes, November 2020, +| Matthieu Sozeau for the Coq development team +| + + +Changes in 8.13 +~~~~~~~~~~~~~~~ + +.. contents:: + :local: + +Kernel +^^^^^^ + +- **Added:** + Definitional UIP, only when :flag:`Definitional UIP` is enabled. See + documentation of the flag for details. + (`#10390 `_, + by Gaëtan Gilbert). +- **Added:** + Built-in support for persistent arrays, which expose a functional + interface but are implemented using an imperative data structure, for + better performance. + (`#11604 `_, + by Maxime Dénès and Benjamin Grégoire, with help from 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 `_, fixes `#12525 + `_ and `#12647 + `_, by Hugo Herbelin). +- **Changed:** Primitive arrays are now irrelevant in their single + polymorphic universe (same as a polymorphic cumulative list + inductive would be) (`#13356 + `_, fixes `#13354 + `_, by Gaëtan Gilbert). + +Specification language, type inference +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **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 `_, by Matthieu + Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and + Enrico Tassi, fixes `#4095 `_ and + `#4413 `_). +- **Changed:** Heuristics for universe minimization to :g:`Set`: also + use constraints ``Prop <= i`` (`#10331 + `_, by Gaëtan Gilbert with + help from Maxime Dénès and Matthieu Sozeau, fixes `#12414 + `_). + + .. _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 ` + mode) (`#12653 `_, 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 `_, + fixes `#12001 `_ + and `#6785 `_, + by Jasper Hugunin). + + .. _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 `_, + fixes `#12762 `_, + by Hugo Herbelin). +- **Removed:** + Undocumented and experimental forward class hint feature ``:>>``. + Use ``:>`` (see :n:`@of_type`) instead + (`#13106 `_, + by Pierre-Marie Pédrot). +- **Fixed:** + Implicit arguments taken into account in defined fields of a record type declaration + (`#13166 `_, + fixes `#13165 `_, + 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 `_, + by Enrico Tassi). +- **Removed:** The type given to :cmd:`Instance` is no longer automatically + generalized over unbound and :ref:`generalizable ` 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 `_, fixes `#6042 + `_, by Gaëtan Gilbert). +- **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 `_, + fixes `#13216 `_, + by Hugo Herbelin). +- **Added:** + Inference of return predicate of a :g:`match` by inversion takes + sort elimination constraints into account + (`#13290 `_, + grants `#13278 `_, + by Hugo Herbelin). + + .. _813BooleanAttrs: + +- **Changed:** + :term:`Boolean attributes ` 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) `, + :attr:`universes(template=no) ` + and :attr:`universes(cumulative=no) `. + 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 `_, + by Emilio Jesus Gallego Arias). +- **Fixed:** + A case of unification raising an anomaly IllTypedInstance + (`#13376 `_, + fixes `#13266 `_, + by Hugo Herbelin). +- **Fixed:** + Using :n:`{wf ...}` in local fixpoints is an error, not an anomaly + (`#13383 `_, + fixes `#11816 `_, + by Hugo Herbelin). +- **Fixed:** + issue when two expressions involving different projections and one is + primitive need to be unified + (`#13386 `_, + fixes `#9971 `_, + by Hugo Herbelin). +- **Fixed:** + A bug producing ill-typed instances of existential variables when let-ins + interleaved with assumptions + (`#13387 `_, + fixes `#12348 `_, + 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 `_, + fixes `#9514 `_, + by Hugo Herbelin). +- **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 `_, + by Pierre Roux). +- **Changed:** + Improved support for notations/abbreviations with mixed terms and patterns (such as the forcing modality) + (`#12099 `_, + by Hugo Herbelin). +- **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 ` and :ref:`String Notation + ` commands now + support parameterized inductive and non inductive types + (`#12218 `_, + fixes `#12035 `_, + by Pierre Roux, review by Jason Gross and Jim Fehrle for the + reference manual). +- **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 + `_, by Hugo Herbelin). +- **Added:** + Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` + (`#12765 `_, + 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 `_, + fixes `#4738 `_ + and `#9682 `_ + and part 2 of `#12908 `_, + by Hugo Herbelin). +- **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 `_, + fixes `#9403 `_ + and `#10803 `_, + by Hugo Herbelin). +- **Fixed:** + Capture of the name of global references by + binders in the presence of notations for binders + (`#12965 `_, + fixes `#9569 `_, + by Hugo Herbelin). +- **Deprecated:** + :n:`Numeral Notation`, please use :ref:`Number Notation ` instead. + (`#12979 `_, + by Pierre Roux). +- **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 + `_ of a priority given to + notations which match a larger part of the term to print + (`#12984 `_, + fixes `#7443 `_ + and `#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 `_, + by Hugo Herbelin). +- **Fixed:** + Preventing notations for constructors to involve binders + (`#13092 `_, + fixes `#13078 `_, + by Hugo Herbelin). +- **Added:** + The :n:`@binder` entry of :cmd:`Notation` can now be used in + notations expecting a single (non-recursive) binder + (`#13265 `_, + by Hugo Herbelin, see section :n:`notations-and-binders` of the + reference manual). +- **Fixed:** Notations understand universe names without getting + confused by different imported modules between declaration and use + locations (`#13415 `_, fixes + `#13303 `_, by Gaëtan + Gilbert). + +Tactics +^^^^^^^ + +- **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 `_, by Frédéric Besson). +- **Added:** + `apply in` supports several hypotheses + (`#12246 `_, + by Hugo Herbelin; grants + `#9816 `_). +- **Removed:** + The deprecated and undocumented "prolog" tactic was removed + (`#12399 `_, + by Pierre-Marie Pédrot). +- **Removed:** Removed info tactic that was deprecated in 8.5. + (`#12423 `_, by Jim Fehrle). +- **Added:** + Thhe :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` + tactic. (`#12552 `_, + by Kazuhiko Sakaguchi). +- **Added:** + The :tacn:`zify` tactic provides support for primitive integers (module :g:`ZifyInt63`). + (`#12648 `_, by Frédéric Besson). +- **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 `_, + fixes `#13235 `_, + by Hugo Herbelin). +- **Fixed:** + Avoiding exposing an internal name of the form :n:`_tmp` when applying the + :n:`_` introduction pattern would break a dependency + (`#13337 `_, + fixes `#13336 `_, + by Hugo Herbelin). +- **Fixed:** + The case of tactics, such as :tacn:`eapply`, producing existential variables + under binders with an ill-formed instance + (`#13373 `_, + fixes `#13363 `_, + by Hugo Herbelin). +- **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 `_, + by Jim Fehrle). +- **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 `_, + 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 `_, + by Jim Fehrle). + +Tactic language +^^^^^^^^^^^^^^^ + +- **Fixed:** + printing of the quotation qualifiers when printing :g:`Ltac` functions + (`#13028 `_, + fixes `#9716 `_ + and `#13004 `_, + by Hugo Herbelin). +- **Added:** + An if-then-else syntax to Ltac2 + (`#13232 `_, + fixes `#10110 `_, + by Pierre-Marie Pédrot). + +SSReflect +^^^^^^^^^ + +- **Added:** + SSReflect intro pattern ltac views ``/[dup]``, ``/[swap]`` and ``/[apply]`` + (`#13317 `_, + by Cyril Cohen). +- **Fixed:** + Working around a bug of interaction between + and /(ltac:(...)) cf #13458 + (`#13459 `_, + by Cyril Cohen). + +Commands and options +^^^^^^^^^^^^^^^^^^^^ + +- **Deprecated:** + :cmd:`Grab Existential Variables` and :cmd:`Existential` commands + (`#12516 `_, + by Maxime Dénès). +- **Removed:** + In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. + Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 `_ + (`#13016 `_, by Jim Fehrle). +- **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 `_, + fixes `#11277 `_, + by Emilio Jesus Gallego Arias). +- **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 `_, + by Jim Fehrle). +- **Changed:** + When declaring arbitrary terms as hints, unsolved + evars are not abstracted implicitly anymore and instead + raise an error + (`#13139 `_, + by Pierre-Marie Pédrot). +- **Added:** + Added support for automatic insertion of coercions in :cmd:`Search` + patterns. Additionally, head patterns are now automatically + interpreted as types + (`#13255 `_, + fixes `#13244 `_, + by Hugo Herbelin). +- **Added:** + The :cmd:`Proof using` command can now be used without loading the + Ltac plugin (`-noinit` mode) + (`#13339 `_, + by Théo Zimmermann). +- **Added:** + Clarify in the documentation that :cmd:`Add ML Path` is not exported to compiled files + (`#13345 `_, + fixes `#13344 `_, + by Hugo Herbelin). +- **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 `_ + (`#13352 `_, + by Pierre Roux). +- **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 `_, + by Pierre-Marie Pédrot). +- **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 `_, + by Pierre-Marie Pédrot). + +Tools +^^^^^ + +- **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 `_, by Martin Bodin, review of Enrico Tassi). +- **Changed:** + ``dev/tools/make-changelog.sh`` now asks for a list of bugs fixed by the PR + (`#12410 `_, fixes `#12386 + `_, by Jason Gross). +- **Removed:** The option ``-I`` of coqchk was removed (it was + deprecated in Coq 8.8) (`#12613 + `_, by Gaëtan Gilbert). +- **Fixed:** + ``coqchk`` no longer reports names from inner modules of opaque modules as + axioms (`#12862 `_, fixes `#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 `_, + by Jim Fehrle and Enrico Tassi) +- **Added:** + Support for flag :flag:`Printing Goal Names` in View menu + (`#13145 `_, + by Hugo Herbelin). + +Standard library +^^^^^^^^^^^^^^^^ + +- **Added:** + Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. + (`#12094 `_, + fixes `#12093 `_, + by Edward Wang). +- **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 `_, + by Michael Soegtrop). +- **Added:** + ``Decidable`` instance for negation + (`#12420 `_, + by Yishuai Li). +- **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 `_, fixes + `#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 + `_, fixes `#12454 + `_, by Jason Gross). +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#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 `_, + by Olivier Laurent). +- **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 `_, + 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 `_, + fixes `#12860 `_, + by Jason Gross). +- **Fixed:** + `Coq.Program.Wf.Fix_F_inv` and `Coq.Program.Wf.Fix_eq` are now axiom-free. They no longer assume proof irrelevance. + (`#13365 `_, + by Li-yao Xia). + +Infrastructure and dependencies +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +- **Changed:** + Coq's core system now uses the `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 `_, + by Emilio Jesus Gallego Arias and Vicent Laporte). +- **Removed:** + The `num` library is not linked to Coq anymore + (`#13007 `_, + by Emilio Jesus Gallego Arias). + +Miscellaneous +^^^^^^^^^^^^^ + + .. _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 `_, + by Emilio Jesus Gallego Arias). + Version 8.12 ------------ -- cgit v1.2.3 From 2dbc0f240a861870c5d59e35749b446b0fe824bf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Dec 2020 14:51:15 +0100 Subject: Add an anchor in syntax-extensions --- doc/sphinx/user-extensions/syntax-extensions.rst | 2 ++ 1 file changed, 2 insertions(+) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index df73de846f..64deb692fd 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -588,6 +588,8 @@ As an exception, if the right-hand side is just of the form :n:`@@qualid`, this conventionally stops the inheritance of implicit arguments (but not of notation scopes). +.. _notations-and-binders: + Notations and binders ~~~~~~~~~~~~~~~~~~~~~ -- cgit v1.2.3 From c8fc6b8f0d357b01f919b8346f45d0bd020f4fe2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 30 Nov 2020 10:03:47 +0100 Subject: [changelog] update markup --- doc/changelog/01-kernel/00000-title.rst | 3 ++- doc/changelog/02-specification-language/00000-title.rst | 3 ++- doc/changelog/03-notations/00000-title.rst | 3 ++- doc/changelog/04-tactics/00000-title.rst | 3 ++- doc/changelog/05-tactic-language/00000-title.rst | 3 ++- doc/changelog/06-ssreflect/00000-title.rst | 3 ++- doc/changelog/07-commands-and-options/00000-title.rst | 3 ++- doc/changelog/08-tools/00000-title.rst | 3 ++- doc/changelog/09-coqide/00000-title.rst | 3 ++- doc/changelog/10-standard-library/00000-title.rst | 3 ++- doc/changelog/11-infrastructure-and-dependencies/00000-title.rst | 3 ++- doc/changelog/12-misc/00000-title.rst | 3 ++- 12 files changed, 24 insertions(+), 12 deletions(-) diff --git a/doc/changelog/01-kernel/00000-title.rst b/doc/changelog/01-kernel/00000-title.rst index f680628a05..287382eab0 100644 --- a/doc/changelog/01-kernel/00000-title.rst +++ b/doc/changelog/01-kernel/00000-title.rst @@ -1,3 +1,4 @@ -**Kernel** +Kernel +^^^^^^ diff --git a/doc/changelog/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/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/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/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/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/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/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/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/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/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/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 +^^^^^^^^^^^^^ -- cgit v1.2.3 From 554a3b171e33a649c65a509046387b86615b4348 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Dec 2020 14:49:18 +0100 Subject: Apply suggestions from @jfehrle code review Co-authored-by: Jim Fehrle --- doc/sphinx/changes.rst | 44 ++++++++++++++++++++++---------------------- 1 file changed, 22 insertions(+), 22 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index e97fba3546..0626f240fd 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -237,7 +237,6 @@ Specification language, type inference 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 `_, by Emilio Jesus Gallego Arias). - **Fixed:** @@ -251,7 +250,8 @@ Specification language, type inference fixes `#11816 `_, by Hugo Herbelin). - **Fixed:** - issue when two expressions involving different projections and one is + + Issue when two expressions involving different projections and one is primitive need to be unified (`#13386 `_, fixes `#9971 `_, @@ -296,7 +296,7 @@ Notations 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 + 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``). - **Removed** OCaml parser and printer for real constants have been removed. @@ -338,7 +338,7 @@ Notations and `#10803 `_, by Hugo Herbelin). - **Fixed:** - Capture of the name of global references by + Capture the names of global references by binders in the presence of notations for binders (`#12965 `_, fixes `#9569 `_, @@ -348,10 +348,10 @@ Notations (`#12979 `_, by Pierre Roux). - **Changed:** - Redeclaring a notation reactivates also its printing rule; in + 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 of behavior for printing. However, this is mitigated in + changes in behavior for printing. However, this is mitigated in general by the adoption in `#12986 `_ of a priority given to notations which match a larger part of the term to print @@ -373,7 +373,7 @@ Notations The :n:`@binder` entry of :cmd:`Notation` can now be used in notations expecting a single (non-recursive) binder (`#13265 `_, - by Hugo Herbelin, see section :n:`notations-and-binders` of the + by Hugo Herbelin, see section :ref:`notations-and-binders` of the reference manual). - **Fixed:** Notations understand universe names without getting confused by different imported modules between declaration and use @@ -389,7 +389,7 @@ Tactics (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) (`#11906 `_, by Frédéric Besson). - **Added:** - `apply in` supports several hypotheses + :tacn`apply … in` supports several hypotheses (`#12246 `_, by Hugo Herbelin; grants `#9816 `_). @@ -397,10 +397,10 @@ Tactics The deprecated and undocumented "prolog" tactic was removed (`#12399 `_, by Pierre-Marie Pédrot). -- **Removed:** Removed info tactic that was deprecated in 8.5. +- **Removed:** Removed `info` tactic that was deprecated in 8.5. (`#12423 `_, by Jim Fehrle). - **Added:** - Thhe :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` + The :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` tactic. (`#12552 `_, by Kazuhiko Sakaguchi). - **Added:** @@ -414,7 +414,7 @@ Tactics by Hugo Herbelin). - **Fixed:** Avoiding exposing an internal name of the form :n:`_tmp` when applying the - :n:`_` introduction pattern would break a dependency + :n:`_` introduction pattern which would break a dependency (`#13337 `_, fixes `#13336 `_, by Hugo Herbelin). @@ -431,7 +431,7 @@ Tactics (`#13381 `_, by Jim Fehrle). - **Removed:** - :n:`at @occs_nums` clauses in tactics such as tacn:`unfold` + :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. @@ -449,7 +449,7 @@ Tactic language ^^^^^^^^^^^^^^^ - **Fixed:** - printing of the quotation qualifiers when printing :g:`Ltac` functions + Printing of the quotation qualifiers when printing :g:`Ltac` functions (`#13028 `_, fixes `#9716 `_ and `#13004 `_, @@ -488,7 +488,7 @@ Commands and options 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. + variable and report back on good settings so we can improve the defaults. (`#13040 `_, fixes `#11277 `_, by Emilio Jesus Gallego Arias). @@ -522,12 +522,12 @@ Commands and options fixes `#13344 `_, by Hugo Herbelin). - **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 + 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 is added as an on demand value, which becomes the default, thus preserving the previous default behavior. - The stdlib is still precompiled when configuring with -native-compiler + 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 `_ @@ -543,8 +543,8 @@ Commands and options by Pierre-Marie Pédrot). - **Changed:** The :attr:`export` locality can now be used for all Hint commands, - including Hint Cut, Hint Mode, Hint Transparent / Opaque and - Remove Hints + including :tacn:`Hint Cut`, :tacn:`Hint Mode`, :tacn:`Hint Transparent` / `Opaque` and + :tacn:`Remove Hints` (`#13388 `_, by Pierre-Marie Pédrot). @@ -552,7 +552,7 @@ Tools ^^^^^ - **Changed:** - Adding the possibility in coq_makefile to directly set the installation folders, + Added the ability for coq_makefile to directly set the installation folders, through the :n:`COQLIBINSTALL` and :n:`COQDOCINSTALL` variables. See :ref:`coqmakefilelocal`. (`#12389 `_, by Martin Bodin, review of Enrico Tassi). @@ -648,7 +648,7 @@ Infrastructure and dependencies Coq's core system now uses the `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 + not longer provided; note that ``micromega`` still uses ``num`` (`#11742 `_, by Emilio Jesus Gallego Arias and Vicent Laporte). -- cgit v1.2.3 From e9b3040326632589d811253e91de4f27c9cf70b4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Dec 2020 15:05:35 +0100 Subject: Changes without PR references fixes --- doc/sphinx/changes.rst | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 0626f240fd..c9968a64b2 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -292,15 +292,21 @@ Notations by Hugo Herbelin). - **Deprecated** ``Numeral.v`` is deprecated, please use ``Number.v`` instead. + (`#12218 `_, + by Pierre Roux). - **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 `_, + by Pierre Roux). - **Removed** OCaml parser and printer for real constants have been removed. Real constants are now handled with proven Coq code. + (`#12218 `_, + by Pierre Roux). - **Added:** :ref:`Number Notation ` and :ref:`String Notation ` commands now @@ -543,8 +549,8 @@ Commands and options by Pierre-Marie Pédrot). - **Changed:** The :attr:`export` locality can now be used for all Hint commands, - including :tacn:`Hint Cut`, :tacn:`Hint Mode`, :tacn:`Hint Transparent` / `Opaque` and - :tacn:`Remove Hints` + including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / `Opaque` and + :cmd:`Remove Hints` (`#13388 `_, by Pierre-Marie Pédrot). -- cgit v1.2.3 From f23ccddcf3bb72d190cfb05e7b48bee416eb8a42 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Dec 2020 15:08:20 +0100 Subject: Fixes in the summary by Jim Fehrle Co-authored-by: Jim Fehrle --- doc/sphinx/changes.rst | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index c9968a64b2..674adb2038 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -25,8 +25,8 @@ The main changes include: (deactivated by default). This models definitional uniqueness of identity proofs for this type. It is deactivated by default as it results in non-termination in combination with impredicativity. - Use of this flag is also shown by :cmd:`Print Assumptions`. - - Cumulative record and inductives type declarations can now + Use of this flag is also printed by :cmd:`Print Assumptions`. + - 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 @@ -50,6 +50,8 @@ The main changes include: now supporting reasoning on boolean operators such as `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. See the `Changes in 8.13`_ section and following sections for the detailed list of changes, including potentially breaking changes marked @@ -93,7 +95,7 @@ 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, Théo Zimmermann. +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 @@ -102,7 +104,7 @@ coqdev@inria.fr, the coq-club@inria.fr mailing list, the `Discourse forum 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 PRs merged, closing ~100 issues. +This release is the result of 400 merged PRs, closing ~100 issues. | Nantes, November 2020, | Matthieu Sozeau for the Coq development team -- cgit v1.2.3 From 002ab0b6bdf38c4dea0ce74e2a0df1e3d2bc238d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Dec 2020 15:15:38 +0100 Subject: Update doc/sphinx/changes.rst Co-authored-by: Jim Fehrle --- doc/sphinx/changes.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 674adb2038..6facb0e207 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -35,7 +35,7 @@ The main changes include: multiple distinct patterns. - New warning for `Hint` commands outside sections without a locality attribute, whose goal is to eventually remove the fragile default - behavior of having hints be imported when using `Require` only. + 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`. -- cgit v1.2.3 From 73eb97c9067caabe5dc93bbb4c5e68b5783f1787 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Dec 2020 17:02:20 +0100 Subject: Apply suggestions from code review Co-authored-by: Jim Fehrle --- doc/sphinx/changes.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6facb0e207..9a2e1b686b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -83,7 +83,7 @@ Georges Gonthier, Benjamin Grégoire, Jason Gross, Hugo Herbelin, Vincent Laporte, 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, Théo Zimmermann +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, @@ -535,8 +535,8 @@ Commands and options `-native-compiler` option of the configure script is added as an on demand 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. + 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 `_ (`#13352 `_, -- cgit v1.2.3 From dba9b80b25a75b9f210f87d4c1f58bc95ef33fa9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 2 Dec 2020 16:31:59 +0100 Subject: Apply suggestions from code review Co-authored-by: Théo Zimmermann --- doc/sphinx/changes.rst | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 9a2e1b686b..0ae80e0685 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -111,8 +111,8 @@ This release is the result of 400 merged PRs, closing ~100 issues. | -Changes in 8.13 -~~~~~~~~~~~~~~~ +Changes in 8.13+beta1 +~~~~~~~~~~~~~~~~~~~~~ .. contents:: :local: @@ -212,7 +212,7 @@ Specification language, type inference (`#13188 `_, fixes `#6042 `_, by Gaëtan Gilbert). - **Fixed:** - Allow use of type classes inference for the return predicate of a :n:`match` + Allow use of typeclass inference for the return predicate of a :n:`match` (was deactivated in versions 8.10 to 8.12, `#13217 `_, fixes `#13216 `_, by Hugo Herbelin). @@ -252,7 +252,6 @@ Specification language, type inference fixes `#11816 `_, by Hugo Herbelin). - **Fixed:** - Issue when two expressions involving different projections and one is primitive need to be unified (`#13386 `_, @@ -319,8 +318,8 @@ Notations reference manual). - **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 + 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 `_, by Hugo Herbelin). - **Added:** @@ -352,7 +351,7 @@ Notations fixes `#9569 `_, by Hugo Herbelin). - **Deprecated:** - :n:`Numeral Notation`, please use :ref:`Number Notation ` instead. + `Numeral Notation`, please use :cmd:`Number Notation` instead (`#12979 `_, by Pierre Roux). - **Changed:** @@ -397,15 +396,15 @@ Tactics (As `lia` gets more powerful, this may break proof scripts relying on `lia` failure.) (`#11906 `_, by Frédéric Besson). - **Added:** - :tacn`apply … in` supports several hypotheses + :tacn:`apply … in` supports several hypotheses (`#12246 `_, by Hugo Herbelin; grants `#9816 `_). - **Removed:** - The deprecated and undocumented "prolog" tactic was removed + The deprecated and undocumented `prolog` tactic was removed (`#12399 `_, by Pierre-Marie Pédrot). -- **Removed:** Removed `info` tactic that was deprecated in 8.5. +- **Removed:** `info` tactic that was deprecated in 8.5. (`#12423 `_, by Jim Fehrle). - **Added:** The :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` @@ -421,7 +420,7 @@ Tactics fixes `#13235 `_, by Hugo Herbelin). - **Fixed:** - Avoiding exposing an internal name of the form :n:`_tmp` when applying the + Avoid exposing an internal name of the form :n:`_tmp` when applying the :n:`_` introduction pattern which would break a dependency (`#13337 `_, fixes `#13336 `_, @@ -476,7 +475,8 @@ SSReflect (`#13317 `_, by Cyril Cohen). - **Fixed:** - Working around a bug of interaction between + and /(ltac:(...)) cf #13458 + Working around a bug of interaction between + and /(ltac:(...)) cf + `#13458 `_ (`#13459 `_, by Cyril Cohen). -- cgit v1.2.3 From d6f42354bc4c0129ee067052c40a5f62a6783c52 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 2 Dec 2020 17:18:15 +0100 Subject: Implement suggestions by Théo Zimmermann --- doc/sphinx/changes.rst | 444 +++++++++++++++++++++++++------------------------ 1 file changed, 228 insertions(+), 216 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 0ae80e0685..b5fb2cbcec 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -18,26 +18,26 @@ Coq version 8.13 integrates many usability improvements, as well as extensions of the core language. The main changes include: - - Introduction of :ref:`primitive persistent arrays` + - :ref:`Introduction <813PrimArrays>` of :ref:`primitive persistent arrays` in the core language, implemented using imperative persistent arrays. - - Introduction of definitional proof irrelevance for the equality type + - Introduction of :ref:`definitional proof irrelevance <813UIP>` for the equality type defined in the SProp sort, using the :flag:`Definitional UIP` flag, (deactivated by default). This models definitional uniqueness of identity proofs for this type. It is deactivated by default as - it results in non-termination in combination with impredicativity. + it can lead to non-termination in combination with impredicativity. Use of this flag is also printed by :cmd:`Print Assumptions`. - Cumulative record and inductive type declarations can now - :ref:`specify<813VarianceDecl>` the variance of their universes. + :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 warning 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 + - 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 `_ for details. @@ -46,14 +46,15 @@ The main changes include: 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 improvements in :tacn:`lia` and its :tacn:`zify` preprocessing step, - now supporting reasoning on boolean operators such as `Z.leb` and supporting + - 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. + - 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`_ section and following sections for the +See the `Changes in 8.13+beta1`_ section and following sections for the detailed list of changes, including potentially breaking changes marked with **Changed**. @@ -75,15 +76,15 @@ 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/. -TODO updated maintainers -Our current 31 maintainers are Yves Bertot, Frédéric Besson, Tej +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, 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 +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, @@ -120,17 +121,29 @@ Changes in 8.13+beta1 Kernel ^^^^^^ + .. _813UIP: + - **Added:** Definitional UIP, only when :flag:`Definitional UIP` is enabled. See documentation of the flag for details. (`#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 `_, 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 + `_, fixes `#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 @@ -139,37 +152,39 @@ Kernel (`#12537 `_, fixes `#12525 `_ and `#12647 `_, by Hugo Herbelin). -- **Changed:** Primitive arrays are now irrelevant in their single - polymorphic universe (same as a polymorphic cumulative list - inductive would be) (`#13356 - `_, fixes `#13354 - `_, by Gaëtan Gilbert). Specification language, type inference ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + .. _813BooleanAttrs: + - **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 `_, by Matthieu - Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and - Enrico Tassi, fixes `#4095 `_ and - `#4413 `_). + :term:`Boolean attributes ` 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) `, + :attr:`universes(template=no) ` + and :attr:`universes(cumulative=no) `. + 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 `_, + by Emilio Jesus Gallego Arias). - **Changed:** Heuristics for universe minimization to :g:`Set`: also use constraints ``Prop <= i`` (`#10331 `_, by Gaëtan Gilbert with help from Maxime Dénès and Matthieu Sozeau, fixes `#12414 `_). - - .. _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 ` - mode) (`#12653 `_, by Gaëtan - Gilbert). +- **Changed:** The type given to :cmd:`Instance` is no longer automatically + generalized over unbound and :ref:`generalizable ` variables. + Use ``Instance : `{type}`` instead of :n:`Instance : @type` to get the old behaviour, or + enable the compatibility flag :flag:`Instance Generalized Output`. + (`#13188 `_, fixes `#6042 + `_, by Gaëtan Gilbert). - **Changed:** Tweaked the algorithm giving default names to arguments. Should reduce the frequency that argument names get an @@ -179,6 +194,19 @@ Specification language, type inference fixes `#12001 `_ and `#6785 `_, by Jasper Hugunin). +- **Removed:** + Undocumented and experimental forward class hint feature ``:>>``. + Use ``:>`` (see :n:`@of_type`) instead + (`#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 ` + mode) (`#12653 `_, by Gaëtan + Gilbert). .. _813UnusedVar: @@ -189,58 +217,28 @@ Specification language, type inference (`#12768 `_, fixes `#12762 `_, by Hugo Herbelin). -- **Removed:** - Undocumented and experimental forward class hint feature ``:>>``. - Use ``:>`` (see :n:`@of_type`) instead - (`#13106 `_, - by Pierre-Marie Pédrot). -- **Fixed:** - Implicit arguments taken into account in defined fields of a record type declaration - (`#13166 `_, - fixes `#13165 `_, - 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 `_, by Enrico Tassi). -- **Removed:** The type given to :cmd:`Instance` is no longer automatically - generalized over unbound and :ref:`generalizable ` 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 `_, fixes `#6042 - `_, by Gaëtan Gilbert). -- **Fixed:** - Allow use of typeclass inference for the return predicate of a :n:`match` - (was deactivated in versions 8.10 to 8.12, `#13217 `_, - fixes `#13216 `_, - by Hugo Herbelin). - **Added:** Inference of return predicate of a :g:`match` by inversion takes sort elimination constraints into account (`#13290 `_, grants `#13278 `_, by Hugo Herbelin). - - .. _813BooleanAttrs: - -- **Changed:** - :term:`Boolean attributes ` 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) `, - :attr:`universes(template=no) ` - and :attr:`universes(cumulative=no) `. - 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 `_, - by Emilio Jesus Gallego Arias). +- **Fixed:** + Implicit arguments taken into account in defined fields of a record type declaration + (`#13166 `_, + fixes `#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 `_, + fixes `#13216 `_, + by Hugo Herbelin). - **Fixed:** A case of unification raising an anomaly IllTypedInstance (`#13376 `_, @@ -282,19 +280,10 @@ Notations (`#11841 `_, fixes `#9514 `_, by Hugo Herbelin). -- **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 `_, - by Pierre Roux). - **Changed:** Improved support for notations/abbreviations with mixed terms and patterns (such as the forcing modality) (`#12099 `_, by Hugo Herbelin). -- **Deprecated** - ``Numeral.v`` is deprecated, please use ``Number.v`` instead. - (`#12218 `_, - by Pierre Roux). - **Changed** Rational and real constants are parsed differently. The exponent is now encoded separately from the fractional part @@ -303,29 +292,12 @@ Notations were parsed (i.e., ``102e-2`` is reprinted as such and not ``1.02``). (`#12218 `_, by Pierre Roux). -- **Removed** - OCaml parser and printer for real constants have been removed. - Real constants are now handled with proven Coq code. - (`#12218 `_, - by Pierre Roux). -- **Added:** - :ref:`Number Notation ` and :ref:`String Notation - ` commands now - support parameterized inductive and non inductive types - (`#12218 `_, - fixes `#12035 `_, - by Pierre Roux, review by Jason Gross and Jim Fehrle for the - reference manual). - **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 `_, by Hugo Herbelin). -- **Added:** - Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` - (`#12765 `_, - 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 @@ -336,24 +308,6 @@ Notations and `#9682 `_ and part 2 of `#12908 `_, by Hugo Herbelin). -- **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 `_, - fixes `#9403 `_ - and `#10803 `_, - by Hugo Herbelin). -- **Fixed:** - Capture the names of global references by - binders in the presence of notations for binders - (`#12965 `_, - fixes `#9569 `_, - by Hugo Herbelin). -- **Deprecated:** - `Numeral Notation`, please use :cmd:`Number Notation` instead - (`#12979 `_, - by Pierre Roux). - **Changed:** Redeclaring a notation also reactivates its printing rule; in particular a second :cmd:`Import` of the same module reactivates the @@ -371,10 +325,35 @@ Notations to notations which match a larger part of the term to abbreviate (`#12986 `_, by Hugo Herbelin). -- **Fixed:** - Preventing notations for constructors to involve binders - (`#13092 `_, - fixes `#13078 `_, +- **Removed** + OCaml parser and printer for real constants have been removed. + Real constants are now handled with proven Coq code. + (`#12218 `_, + by Pierre Roux). +- **Deprecated** + ``Numeral.v`` is deprecated, please use ``Number.v`` instead. + (`#12218 `_, + by Pierre Roux). +- **Deprecated:** + `Numeral Notation`, please use :cmd:`Number Notation` instead + (`#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 `_, + by Pierre Roux). +- **Added:** + :ref:`Number Notation ` and :ref:`String Notation + ` commands now + support parameterized inductive and non inductive types + (`#12218 `_, + fixes `#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 `_, by Hugo Herbelin). - **Added:** The :n:`@binder` entry of :cmd:`Notation` can now be used in @@ -382,15 +361,77 @@ Notations (`#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 `_, + fixes `#9403 `_ + and `#10803 `_, + by Hugo Herbelin). +- **Fixed:** + Capture the names of global references by + binders in the presence of notations for binders + (`#12965 `_, + fixes `#9569 `_, + by Hugo Herbelin). +- **Fixed:** + Preventing notations for constructors to involve binders + (`#13092 `_, + fixes `#13078 `_, + by Hugo Herbelin). - **Fixed:** Notations understand universe names without getting confused by different imported modules between declaration and use locations (`#13415 `_, fixes `#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 `_, by Matthieu + Sozeau, with help from Maxime Dénès, review by Pierre-Marie Pédrot and + Enrico Tassi, fixes `#4095 `_ and + `#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 `_, + fixes `#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 `_, + 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 `_, + by Jim Fehrle). +- **Removed:** + The deprecated and undocumented `prolog` tactic was removed + (`#12399 `_, + by Pierre-Marie Pédrot). +- **Removed:** `info` tactic that was deprecated in 8.5. + (`#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 `_, + 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.) @@ -400,12 +441,6 @@ Tactics (`#12246 `_, by Hugo Herbelin; grants `#9816 `_). -- **Removed:** - The deprecated and undocumented `prolog` tactic was removed - (`#12399 `_, - by Pierre-Marie Pédrot). -- **Removed:** `info` tactic that was deprecated in 8.5. - (`#12423 `_, by Jim Fehrle). - **Added:** The :tacn:`zify` tactic can now be extended by redefining the `zify_pre_hook` tactic. (`#12552 `_, @@ -413,12 +448,6 @@ Tactics - **Added:** The :tacn:`zify` tactic provides support for primitive integers (module :g:`ZifyInt63`). (`#12648 `_, by Frédéric Besson). -- **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 `_, - fixes `#13235 `_, - by Hugo Herbelin). - **Fixed:** Avoid exposing an internal name of the form :n:`_tmp` when applying the :n:`_` introduction pattern which would break a dependency @@ -431,41 +460,21 @@ Tactics (`#13373 `_, fixes `#13363 `_, by Hugo Herbelin). -- **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 `_, - by Jim Fehrle). -- **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 `_, - 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 `_, - by Jim Fehrle). Tactic language ^^^^^^^^^^^^^^^ +- **Added:** + An if-then-else syntax to Ltac2 + (`#13232 `_, + fixes `#10110 `_, + by Pierre-Marie Pédrot). - **Fixed:** Printing of the quotation qualifiers when printing :g:`Ltac` functions (`#13028 `_, fixes `#9716 `_ and `#13004 `_, by Hugo Herbelin). -- **Added:** - An if-then-else syntax to Ltac2 - (`#13232 `_, - fixes `#10110 `_, - by Pierre-Marie Pédrot). SSReflect ^^^^^^^^^ @@ -483,14 +492,6 @@ SSReflect Commands and options ^^^^^^^^^^^^^^^^^^^^ -- **Deprecated:** - :cmd:`Grab Existential Variables` and :cmd:`Existential` commands - (`#12516 `_, - by Maxime Dénès). -- **Removed:** - In the :cmd:`Extraction Language` command, remove `Ocaml` as a valid value. - Use `OCaml` instead. This was deprecated in Coq 8.8, `#6261 `_ - (`#13016 `_, by Jim Fehrle). - **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 @@ -512,23 +513,6 @@ Commands and options raise an error (`#13139 `_, by Pierre-Marie Pédrot). -- **Added:** - Added support for automatic insertion of coercions in :cmd:`Search` - patterns. Additionally, head patterns are now automatically - interpreted as types - (`#13255 `_, - fixes `#13244 `_, - by Hugo Herbelin). -- **Added:** - The :cmd:`Proof using` command can now be used without loading the - Ltac plugin (`-noinit` mode) - (`#13339 `_, - by Théo Zimmermann). -- **Added:** - Clarify in the documentation that :cmd:`Add ML Path` is not exported to compiled files - (`#13345 `_, - fixes `#13344 `_, - by Hugo Herbelin). - **Changed:** Option `-native-compiler` of the configure script now impacts the default value of the `-native-compiler` option of coqc. The @@ -541,6 +525,19 @@ Commands and options `CEP #48 `_ (`#13352 `_, by Pierre Roux). +- **Changed:** + The :attr:`export` locality can now be used for all Hint commands, + including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / `Opaque` and + :cmd:`Remove Hints` + (`#13388 `_, + 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 `_ + (`#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 @@ -549,12 +546,27 @@ Commands and options use :attr:`export` whenever possible (`#13384 `_, by Pierre-Marie Pédrot). -- **Changed:** - The :attr:`export` locality can now be used for all Hint commands, - including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / `Opaque` and - :cmd:`Remove Hints` - (`#13388 `_, - by Pierre-Marie Pédrot). +- **Deprecated:** + :cmd:`Grab Existential Variables` and :cmd:`Existential` commands + (`#12516 `_, + by Maxime Dénès). +- **Added:** + Added support for automatic insertion of coercions in :cmd:`Search` + patterns. Additionally, head patterns are now automatically + interpreted as types + (`#13255 `_, + fixes `#13244 `_, + by Hugo Herbelin). +- **Added:** + The :cmd:`Proof using` command can now be used without loading the + Ltac plugin (`-noinit` mode) + (`#13339 `_, + by Théo Zimmermann). +- **Added:** + Clarify in the documentation that :cmd:`Add ML Path` is not exported to compiled files + (`#13345 `_, + fixes `#13344 `_, + by Hugo Herbelin). Tools ^^^^^ @@ -592,20 +604,11 @@ CoqIDE Standard library ^^^^^^^^^^^^^^^^ -- **Added:** - Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. - (`#12094 `_, - fixes `#12093 `_, - by Edward Wang). - **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 `_, by Michael Soegtrop). -- **Added:** - ``Decidable`` instance for negation - (`#12420 `_, - by Yishuai Li). - **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 @@ -624,14 +627,6 @@ Standard library get the ``PrimFloat`` notations without unqualifying the various primitives (`#12556 `_, fixes `#12454 `_, by Jason Gross). -- **Deprecated:** - ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` - (`#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 `_, - by Olivier Laurent). - **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. @@ -644,6 +639,23 @@ Standard library (`#12861 `_, fixes `#12860 `_, by Jason Gross). +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#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 `_, + by Olivier Laurent). +- **Added:** + Extend some list lemmas to both directions: `app_inj_tail_iff`, `app_inv_head_iff`, `app_inv_tail_iff`. + (`#12094 `_, + fixes `#12093 `_, + by Edward Wang). +- **Added:** + ``Decidable`` instance for negation + (`#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 `_, -- cgit v1.2.3 From d20e4edab5912eb41b8408c3c8ab7541f4fc7834 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 3 Dec 2020 12:30:27 +0100 Subject: Implement review corrections by Théo Zimmermann --- doc/sphinx/changes.rst | 114 +++++++++++++++++++++++-------------------------- 1 file changed, 53 insertions(+), 61 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index b5fb2cbcec..c2b32afea2 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -21,11 +21,7 @@ The main changes include: - :ref:`Introduction <813PrimArrays>` of :ref:`primitive persistent 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, using the :flag:`Definitional UIP` flag, - (deactivated by default). This models definitional uniqueness of - identity proofs for this type. 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`. + 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 @@ -124,7 +120,11 @@ Kernel .. _813UIP: - **Added:** - Definitional UIP, only when :flag:`Definitional UIP` is enabled. See + 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 `_, by Gaëtan Gilbert). @@ -223,6 +223,16 @@ Specification language, type inference interactive mode. (`#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 `_, + by Emilio Jesus Gallego Arias). + - **Added:** Inference of return predicate of a :g:`match` by inversion takes sort elimination constraints into account @@ -492,15 +502,6 @@ SSReflect Commands and options ^^^^^^^^^^^^^^^^^^^^ -- **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 `_, - fixes `#11277 `_, - by Emilio Jesus Gallego Arias). - **Changed:** Drop prefixes from grammar non-terminal names, e.g. "constr:global" -> "global", "Prim.name" -> "name". @@ -513,24 +514,6 @@ Commands and options raise an error (`#13139 `_, by Pierre-Marie Pédrot). -- **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 is added as an on demand - 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 `_ - (`#13352 `_, - by Pierre Roux). -- **Changed:** - The :attr:`export` locality can now be used for all Hint commands, - including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / `Opaque` and - :cmd:`Remove Hints` - (`#13388 `_, - 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 `_ @@ -551,7 +534,14 @@ Commands and options (`#12516 `_, by Maxime Dénès). - **Added:** - Added support for automatic insertion of coercions in :cmd:`Search` + The :attr:`export` locality can now be used for all Hint commands, + including :cmd:`Hint Cut`, :cmd:`Hint Mode`, :cmd:`Hint Transparent` / + :cmd:`Opaque ` and + :cmd:`Remove Hints` + (`#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 `_, @@ -571,15 +561,23 @@ Commands and options 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 `_ + (`#13352 `_, + by Pierre Roux). - **Changed:** Added the ability for coq_makefile to directly set the installation folders, - through the :n:`COQLIBINSTALL` and :n:`COQDOCINSTALL` variables. + through the `COQLIBINSTALL` and `COQDOCINSTALL` variables. See :ref:`coqmakefilelocal`. (`#12389 `_, by Martin Bodin, review of Enrico Tassi). -- **Changed:** - ``dev/tools/make-changelog.sh`` now asks for a list of bugs fixed by the PR - (`#12410 `_, fixes `#12386 - `_, by Jason Gross). - **Removed:** The option ``-I`` of coqchk was removed (it was deprecated in Coq 8.8) (`#12613 `_, by Gaëtan Gilbert). @@ -627,8 +625,8 @@ Standard library get the ``PrimFloat`` notations without unqualifying the various primitives (`#12556 `_, fixes `#12454 `_, by Jason Gross). -- **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. +- **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 `_, by Vincent Semeria). @@ -665,29 +663,23 @@ Infrastructure and dependencies ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - **Changed:** - Coq's core system now uses the `zarith `_ + 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 `_, + fixes `#11277 `_, + by Emilio Jesus Gallego Arias). +- **Changed:** + Coq now uses the `zarith `_ library, based on GNU's gmp instead of ``num`` which is deprecated upstream. The custom ``bigint`` module is - not longer provided; note that ``micromega`` still uses - ``num`` + no longer provided. (`#11742 `_, - by Emilio Jesus Gallego Arias and Vicent Laporte). -- **Removed:** - The `num` library is not linked to Coq anymore - (`#13007 `_, - by Emilio Jesus Gallego Arias). - -Miscellaneous -^^^^^^^^^^^^^ - - .. _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 `_, - by Emilio Jesus Gallego Arias). + `#13007 `_, + by Emilio Jesus Gallego Arias and Vicent Laporte, with help from + Frédéric Besson). Version 8.12 ------------ -- cgit v1.2.3