From fb30e8880a3027ef1c957df668a906d723e8a8a0 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 16 May 2019 18:20:07 +0200 Subject: `deprecated` attribute support for notations and syntactic definitions We also slightly change the semantics of the `compat` syntax modifier to re-express it in terms of the `deprecated` attribute, and we deprecate it in favor of the latter. --- doc/changelog/03-notations/10180-deprecate-notations.rst | 6 ++++++ doc/sphinx/language/gallina-specification-language.rst | 10 +++++++++- 2 files changed, 15 insertions(+), 1 deletion(-) create mode 100644 doc/changelog/03-notations/10180-deprecate-notations.rst (limited to 'doc') 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..050aa105d8 --- /dev/null +++ b/doc/changelog/03-notations/10180-deprecate-notations.rst @@ -0,0 +1,6 @@ +- The `Notation` and `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 `_, by Maxime Dénès. 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 -- cgit v1.2.3 From 80f3014e8360bc9c5bb21e119930bc989a8ed992 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 6 Jun 2019 14:52:34 +0200 Subject: Update doc/changelog/03-notations/10180-deprecate-notations.rst Co-Authored-By: Théo Zimmermann --- doc/changelog/03-notations/10180-deprecate-notations.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst index 050aa105d8..57548513fe 100644 --- a/doc/changelog/03-notations/10180-deprecate-notations.rst +++ b/doc/changelog/03-notations/10180-deprecate-notations.rst @@ -1,4 +1,4 @@ -- The `Notation` and `Infix` commands now support the `deprecated` +- 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` -- cgit v1.2.3 From 26ed9cb34ea5fc84fb086644a03d016817f30a4a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 6 Jun 2019 22:05:26 +0200 Subject: Update doc/changelog/03-notations/10180-deprecate-notations.rst Co-Authored-By: Théo Zimmermann --- doc/changelog/03-notations/10180-deprecate-notations.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/changelog/03-notations/10180-deprecate-notations.rst b/doc/changelog/03-notations/10180-deprecate-notations.rst index 57548513fe..01f2e893ed 100644 --- a/doc/changelog/03-notations/10180-deprecate-notations.rst +++ b/doc/changelog/03-notations/10180-deprecate-notations.rst @@ -3,4 +3,4 @@ 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 `_, by Maxime Dénès. + (`#10180 `_, by Maxime Dénès). -- cgit v1.2.3