From 6016a980fa2ed33ff9bc49e6000436fe1ce6e260 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 22 Jun 2018 23:42:25 +0200
Subject: 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.".
---
 plugins/ltac/tacinterp.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac/tacinterp.ml')

diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d9ac96d894..77b5b06d44 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1125,17 +1125,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
   | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
   (* For extensions *)
   | TacAlias (loc,(s,l)) ->
-      let (ids, body) = Tacenv.interp_alias s in
+      let alias = Tacenv.interp_alias s in
       let (>>=) = Ftactic.bind in
       let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
       let tac l =
         let addvar x v accu = Id.Map.add x v accu in
-        let lfun = List.fold_right2 addvar ids l ist.lfun in
+        let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
         Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
         let ist = {
           lfun = lfun;
           extra = TacStore.set ist.extra f_trace trace; } in
-        val_interp ist body >>= fun v ->
+        val_interp ist alias.Tacenv.alias_body >>= fun v ->
         Ftactic.lift (tactic_of_value ist v)
       in
       let tac =
@@ -1147,7 +1147,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
          some more elaborate solution will have to be used. *)
       in
       let tac =
-        let len1 = List.length ids in
+        let len1 = List.length alias.Tacenv.alias_args in
         let len2 = List.length l in
         if len1 = len2 then tac
         else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
-- 
cgit v1.2.3