Create section on writing libraries with only deprecated attributes.

1 files changed, 0 insertions, 29 deletions

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.