aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst8
1 files changed, 7 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index ac6a20198..8250b4b3d 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1430,6 +1430,12 @@ 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:
+
+ .. warn:: Tactic @qualid is deprecated since @string. @string.
+
+ .. warn:: Tactic Notation @qualid is deprecated since @string. @string.
+
Here are a few examples:
.. coqtop:: all reset
@@ -1440,7 +1446,7 @@ Here are a few examples:
exact O.
Defined.
- #[deprecated(since="8.9.0", note="use idtac instead")]
+ #[deprecated(since="8.9.0", note="Use idtac instead.")]
Ltac foo := idtac.
Goal True.