Tactic deprecation machinery

We make it possible to deprecate tactics defined by `Ltac`, `Tactic
Notation` or ML.

For the first two variants, we anticipate the syntax of attributes:
`#[deprecated(since = "XX", note = "YY")]`

In ML, the syntax is:

```
let reflexivity_depr =
  let open CWarnings in
  { since = "8.5"; note = "Use admit instead." }

TACTIC EXTEND reflexivity DEPRECATED reflexivity_depr
  [ "reflexivity" ] -> [ Tactics.intros_reflexivity ]
END
```

A warning is shown at the point where the tactic is used (either
a direct call or when defining another tactic):

Tactic `foo` is deprecated since XX. YY

YY is typically meant to be "Use bar instead.".

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.