diff options
Diffstat (limited to 'doc/changelog/02-specification-language')
10 files changed, 30 insertions, 18 deletions
diff --git a/doc/changelog/02-specification-language/10049-bidi-app.rst b/doc/changelog/02-specification-language/10049-bidi-app.rst index 279bb9272a..024795f5da 100644 --- a/doc/changelog/02-specification-language/10049-bidi-app.rst +++ b/doc/changelog/02-specification-language/10049-bidi-app.rst @@ -1,4 +1,5 @@ -- New annotation in `Arguments` for bidirectionality hints: it is now possible +- **Added:** + Annotation in `Arguments` for bidirectionality hints: it is now possible to tell type inference to use type information from the context once the `n` first arguments of an application are known. The syntax is: `Arguments foo x y & z`. See :cmd:`Arguments (bidirectionality hints)` diff --git a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst index 0a902079b9..389ee4fd7f 100644 --- a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst +++ b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst @@ -1,4 +1,5 @@ -- Record fields can be annotated to prevent them from being used as canonical projections; +- **Added:** + Record fields can be annotated to prevent them from being used as canonical projections; see :ref:`canonicalstructures` for details (`#10076 <https://github.com/coq/coq/pull/10076>`_, by Vincent Laporte). diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst index 2d17e569d3..87e4c9ff10 100644 --- a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst +++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst @@ -1,11 +1,14 @@ -- Require parentheses around nested disjunctive patterns, so that pattern and +- **Changed:** + Require parentheses around nested disjunctive patterns, so that pattern and term syntax are consistent; match branch patterns no longer require - parentheses for notation at level 100 or more. Incompatibilities: + parentheses for notation at level 100 or more. - + in :g:`match p with (_, (0|1)) => ...` parentheses may no longer be - omitted around :n:`0|1`. - + notation :g:`(p | q)` now potentially clashes with core pattern syntax, - and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. + .. warning:: Incompatibilities + + + In :g:`match p with (_, (0|1)) => ...` parentheses may no longer be + omitted around :n:`0|1`. + + Notation :g:`(p | q)` now potentially clashes with core pattern syntax, + and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. See :ref:`extendedpatternmatching` for details (`#10167 <https://github.com/coq/coq/pull/10167>`_, diff --git a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst index 71b10aaaf4..c201b482e5 100644 --- a/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst +++ b/doc/changelog/02-specification-language/10215-rm-maybe-open-proof.rst @@ -1,9 +1,11 @@ -- :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` +- **Changed:** + :cmd:`Function` always opens a proof when used with a ``measure`` or ``wf`` annotation, see :ref:`advanced-recursive-functions` for the updated documentation (`#10215 <https://github.com/coq/coq/pull/10215>`_, by Enrico Tassi). -- The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used +- **Changed:** + The legacy command :cmd:`Add Morphism` always opens a proof and cannot be used inside a module type. In order to declare a module type parameter that happens to be a morphism, use :cmd:`Declare Morphism`. See :ref:`deprecated_syntax_for_generalized_rewriting` for the updated diff --git a/doc/changelog/02-specification-language/10441-static-poly-section.rst b/doc/changelog/02-specification-language/10441-static-poly-section.rst index 7f0345d946..3d0ca000e6 100644 --- a/doc/changelog/02-specification-language/10441-static-poly-section.rst +++ b/doc/changelog/02-specification-language/10441-static-poly-section.rst @@ -1,11 +1,13 @@ -- The universe polymorphism setting now applies from the opening of a section. +- **Changed:** + The universe polymorphism setting now applies from the opening of a section. In particular, it is not possible anymore to mix polymorphic and monomorphic definitions in a section when there are no variables nor universe constraints defined in this section. This makes the behaviour consistent with the documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) -- The :cmd:`Section` vernacular command now accepts the "universes" attribute. In +- **Added:** + The :cmd:`Section` vernacular command now accepts the "universes" attribute. In addition to setting the section universe polymorphism, it also locally sets the universe polymorphic option inside the section. (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) diff --git a/doc/changelog/02-specification-language/10758-fix-10757.rst b/doc/changelog/02-specification-language/10758-fix-10757.rst index 4cce26aedc..431123ec1b 100644 --- a/doc/changelog/02-specification-language/10758-fix-10757.rst +++ b/doc/changelog/02-specification-language/10758-fix-10757.rst @@ -1,4 +1,5 @@ -- ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes +- **Fixed:** + ``Program Fixpoint`` now uses ``ex`` and ``sig`` to make telescopes involving ``Prop`` types (`#10758 <https://github.com/coq/coq/pull/10758>`_, by Gaëtan Gilbert, fixing `#10757 <https://github.com/coq/coq/issues/10757>`_ reported by diff --git a/doc/changelog/02-specification-language/10985-about-arguments.rst b/doc/changelog/02-specification-language/10985-about-arguments.rst index 1e05b0b0fe..0faaf95e6c 100644 --- a/doc/changelog/02-specification-language/10985-about-arguments.rst +++ b/doc/changelog/02-specification-language/10985-about-arguments.rst @@ -1,5 +1,6 @@ -- The output of the :cmd:`Print` and :cmd:`About` commands has - changed. Arguments meta-data is now displayed as the corresponding +- **Changed:** + Output of the :cmd:`Print` and :cmd:`About` commands. + Arguments meta-data is now displayed as the corresponding :cmd:`Arguments <Arguments (implicits)>` command instead of the human-targeted prose used in previous Coq versions. (`#10985 <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst index cd1a692f54..51a62a0c8d 100644 --- a/doc/changelog/02-specification-language/10996-refine-instance-returns.rst +++ b/doc/changelog/02-specification-language/10996-refine-instance-returns.rst @@ -1,4 +1,4 @@ -- Added ``#[refine]`` attribute for :cmd:`Instance`, a more +- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more predictable version of the old ``Refine Instance Mode`` which unconditionally opens a proof (`#10996 <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst index 43a748b365..49f8f451a7 100644 --- a/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst +++ b/doc/changelog/02-specification-language/10997-unsupport-atts-warn.rst @@ -1,3 +1,4 @@ -- The unsupported attribute error is now an error-by-default warning, +- **Changed:** + The unsupported attribute error is now an error-by-default warning, meaning it can be disabled (`#10997 <https://github.com/coq/coq/pull/10997>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst index f8298cdbdd..6bf261eb9b 100644 --- a/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst +++ b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst @@ -1,4 +1,4 @@ -- Fixed bugs sometimes preventing to define valid (co)fixpoints with implicit arguments +- **Fixed:** Bugs sometimes preventing to define valid (co)fixpoints with implicit arguments in the presence of local definitions, see `#3282 <https://github.com/coq/coq/issues/3282>`_ (`#11132 <https://github.com/coq/coq/pull/11132>`_, by Hugo Herbelin). |