From 57734bc48a98c9dc08b1eebed94363e8c5c8a7b3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 1 May 2020 13:13:05 +0200
Subject: Create section on writing libraries with only deprecated attributes.

---
 .../language/gallina-specification-language.rst    | 29 ----------------------
 doc/sphinx/using/libraries/writing.rst             | 29 ++++++++++++++++++++++
 2 files changed, 29 insertions(+), 29 deletions(-)
 delete mode 100644 doc/sphinx/language/gallina-specification-language.rst
 create mode 100644 doc/sphinx/using/libraries/writing.rst

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
deleted file mode 100644
index 91634ea023..0000000000
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ /dev/null
@@ -1,29 +0,0 @@
-.. 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.
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.
-- 
cgit v1.2.3