Create section on writing libraries with only deprecated attributes.

1 files changed, 29 insertions, 0 deletions

diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst
new file mode 100644
index 0000000000..91634ea023
--- /dev/null
+++ b/doc/sphinx/using/libraries/writing.rst
@@ -0,0 +1,29 @@
+.. attr:: deprecated ( {? since = @string , } {? note = @string } )
+   :name: deprecated
+
+    At least one of :n:`since` or :n:`note` must be present.  If both are present,
+    either one may appear first and they must be separated by a comma.
+
+    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__since. @string__note.
+              Tactic Notation @qualid is deprecated since @string__since. @string__note.
+              Notation @string is deprecated since @string__since. @string__note.
+
+       :n:`@qualid` or :n:`@string` is the notation, :n:`@string__since` is the version number,
+       :n:`@string__note` is the note (usually explains the replacement).
+
+    .. example::
+
+       .. coqtop:: all reset warn
+
+          #[deprecated(since="8.9.0", note="Use idtac instead.")]
+          Ltac foo := idtac.
+
+          Goal True.
+          Proof.
+          now foo.
+          Abort.