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/tacentries.mli | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'plugins/ltac/tacentries.mli')

diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index f873631ffd..138a584e01 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,10 +12,12 @@
 
 open Vernacexpr
 open Tacexpr
+open Vernacinterp
 
 (** {5 Tactic Definitions} *)
 
-val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
+val register_ltac : locality_flag -> ?deprecation:deprecation ->
+  Tacexpr.tacdef_body list -> unit
 (** Adds new Ltac definitions to the environment. *)
 
 (** {5 Tactic Notations} *)
@@ -34,8 +36,8 @@ type argument = Genarg.ArgT.any Extend.user_symbol
     leaves. *)
 
 val add_tactic_notation :
-  locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list ->
-  raw_tactic_expr -> unit
+  locality_flag -> int -> ?deprecation:deprecation -> raw_argument
+  grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit
 (** [add_tactic_notation local level prods expr] adds a tactic notation in the
     environment at level [level] with locality [local] made of the grammar
     productions [prods] and returning the body [expr] *)
@@ -47,7 +49,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -
     to finding an argument by name (as in {!Genarg}) if there is none
     matching. *)
 
-val add_ml_tactic_notation : ml_tactic_name -> level:int ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation ->
   argument grammar_tactic_prod_item_expr list list -> unit
 (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
     ML-side macro. *)
@@ -78,4 +80,5 @@ type _ ty_sig =
 
 type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
-val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit
+val tactic_extend : string -> string -> level:Int.t ->
+  ?deprecation:deprecation -> ty_ml list -> unit
-- 
cgit v1.2.3