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, 32 insertions, 0 deletions

diff --git a/test-suite/success/LtacDeprecation.v b/test-suite/success/LtacDeprecation.v
new file mode 100644
index 000000000..633a5e474
--- /dev/null
+++ b/test-suite/success/LtacDeprecation.v
@@ -0,0 +1,32 @@
+Set Warnings "+deprecated".
+
+#[deprecated(since = "8.8", note = "Use idtac instead")]
+Ltac foo x := idtac.
+
+Goal True.
+Fail (foo true).
+Abort.
+
+Fail Ltac bar := foo.
+Fail Tactic Notation "bar" := foo.
+
+#[deprecated(since = "8.8", note = "Use idtac instead")]
+Tactic Notation "bar" := idtac.
+
+Goal True.
+Fail bar.
+Abort.
+
+Fail Ltac zar := bar.
+
+Set Warnings "-deprecated".
+
+Ltac zar := foo.
+Ltac zarzar := bar.
+
+Set Warnings "+deprecated".
+
+Goal True.
+zar x.
+zarzar.
+Abort.