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, 5 insertions, 1 deletions

diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index cea0bed59..02da61ef7 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -49,13 +49,17 @@ EXTEND
   GLOBAL: str_item;
   str_item:
     [ [ "TACTIC"; "EXTEND"; s = tac_name;
+        depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ];
         level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
         let level = match level with Some i -> int_of_string i | None -> 0 in
         let level = mlexpr_of_int level in
+        let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in
         let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
-        declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ]
+        declare_str_items loc [ <:str_item< Tacentries.tactic_extend
+          $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation =
+          $depr$ } $l$ >> ] ] ]
   ;
   tacrule:
     [ [ "["; l = LIST1 tacargs; "]";