`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.

1 files changed, 9 insertions, 1 deletions

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