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/sphinx/language/gallina-specification-language.rst | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx')

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