diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 8 |
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. |