diff options
Diffstat (limited to 'doc')
4 files changed, 29 insertions, 1 deletions
diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst new file mode 100644 index 0000000000..01f2e893ed --- /dev/null +++ b/doc/changelog/03-notations/10180-deprecate-notations.rst @@ -0,0 +1,6 @@ +- The :cmd:`Notation` and :cmd:`Infix` commands now support the `deprecated` + attribute. The former `compat` annotation for notations is + deprecated, and its semantics changed. It is now made equivalent to using + a `deprecated` attribute, and is no longer connected with the `-compat` + command-line flag. + (`#10180 <https://github.com/coq/coq/pull/10180>`_, by Maxime Dénès). diff --git a/doc/changelog/06-ssreflect/10302-case-HoTT.rst b/doc/changelog/06-ssreflect/10302-case-HoTT.rst new file mode 100644 index 0000000000..686b3c3cca --- /dev/null +++ b/doc/changelog/06-ssreflect/10302-case-HoTT.rst @@ -0,0 +1,7 @@ +- Make the ``case E: t`` tactic work together with + :flag:`Universe Polymorphism` and equality in :g:`Type`. + This makes tacn:`case` compatible with the HoTT + library https://github.com/HoTT/HoTT. + (`#10302 <https://github.com/coq/coq/pull/10302>`_, + fixes `#10301 <https://github.com/coq/coq/issues/10301>`_, + by Andreas Lynge, review by Enrico Tassi) diff --git a/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst b/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst new file mode 100644 index 0000000000..b82de1a879 --- /dev/null +++ b/doc/changelog/06-ssreflect/10305-unfold-HoTT.rst @@ -0,0 +1,7 @@ +- Make the ``rewrite /t`` tactic work together with + :flag:`Universe Polymorphism`. + This makes tacn:`rewrite` compatible with the HoTT + library https://github.com/HoTT/HoTT. + (`#10305 <https://github.com/coq/coq/pull/10305>`_, + fixes `#9336 <https://github.com/coq/coq/issues/9336>`_, + by Andreas Lynge, review by Enrico Tassi) diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index ebaa6fde66..38f6714f46 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1508,7 +1508,10 @@ the following attributes names are recognized: Takes as value the optional attributes ``since`` and ``note``; both have a string value. - This attribute can trigger the following warnings: + This attribute is supported by the following commands: :cmd:`Ltac`, + :cmd:`Tactic Notation`, :cmd:`Notation`, :cmd:`Infix`. + + It can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string. @string. :undocumented: @@ -1516,6 +1519,11 @@ the following attributes names are recognized: .. warn:: Tactic Notation @qualid is deprecated since @string. @string. :undocumented: + .. warn:: Notation @string__1 is deprecated since @string__2. @string__3. + + :n:`@string__1` is the actual notation, :n:`@string__2` is the version number, + :n:`@string__3` is the note. + .. example:: .. coqtop:: all reset warn |