`deprecated` attribute support for notations and syntactic definitions

We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.

4 files changed, 17 insertions, 24 deletions

diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 309db539d0..2cc6f9a279 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,11 +12,10 @@
 
 open Vernacexpr
 open Tacexpr
-open Attributes
 
 (** {5 Tactic Definitions} *)
 
-val register_ltac : locality_flag -> ?deprecation:deprecation ->
+val register_ltac : locality_flag -> ?deprecation:Deprecation.t ->
   Tacexpr.tacdef_body list -> unit
 (** Adds new Ltac definitions to the environment. *)
 
@@ -36,7 +35,7 @@ type argument = Genarg.ArgT.any Extend.user_symbol
     leaves. *)
 
 val add_tactic_notation :
-  locality_flag -> int -> ?deprecation:deprecation -> raw_argument
+  locality_flag -> int -> ?deprecation:Deprecation.t -> 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
@@ -49,7 +48,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 -> ?deprecation:deprecation ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:Deprecation.t ->
   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. *)
@@ -80,7 +79,7 @@ type _ ty_sig =
 type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
 
 val tactic_extend : string -> string -> level:Int.t ->
-  ?deprecation:deprecation -> ty_ml list -> unit
+  ?deprecation:Deprecation.t -> ty_ml list -> unit
 
 (** {5 ARGUMENT EXTEND} *)
 
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index d5f22b2c72..3347f594d2 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -55,7 +55,7 @@ type alias = KerName.t
 type alias_tactic =
   { alias_args: Id.t list;
     alias_body: glob_tactic_expr;
-    alias_deprecation: Attributes.deprecation option;
+    alias_deprecation: Deprecation.t option;
   }
 
 let alias_map = Summary.ref ~name:"tactic-alias"
@@ -121,7 +121,7 @@ type ltac_entry = {
   tac_for_ml : bool;
   tac_body : glob_tactic_expr;
   tac_redef : ModPath.t list;
-  tac_deprecation : Attributes.deprecation option
+  tac_deprecation : Deprecation.t option
 }
 
 let mactab =
@@ -178,7 +178,7 @@ let subst_md (subst, (local, id, b, t, deprecation)) =
 let classify_md (local, _, _, _, _ as o) = Substitute o
 
 let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
-           Attributes.deprecation option -> obj =
+           Deprecation.t option -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 5b98daf383..2fc45760d1 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,7 +12,6 @@ open Names
 open Libnames
 open Tacexpr
 open Geninterp
-open Attributes
 
 (** This module centralizes the various ways of registering tactics. *)
 
@@ -33,7 +32,7 @@ type alias = KerName.t
 type alias_tactic =
   { alias_args: Id.t list;
     alias_body: glob_tactic_expr;
-    alias_deprecation: deprecation option;
+    alias_deprecation: Deprecation.t option;
   }
 (** Contents of a tactic notation *)
 
@@ -48,7 +47,7 @@ val check_alias : alias -> bool
 
 (** {5 Coq tactic definitions} *)
 
-val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t ->
+val register_ltac : bool -> bool -> ?deprecation:Deprecation.t -> Id.t ->
   glob_tactic_expr -> unit
 (** Register a new Ltac with the given name and body.
 
@@ -57,7 +56,7 @@ val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t ->
     definition. It also puts the Ltac name in the nametab, so that it can be
     used unqualified. *)
 
-val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t ->
+val redefine_ltac : bool -> ?deprecation:Deprecation.t -> KerName.t ->
   glob_tactic_expr -> unit
 (** Replace a Ltac with the given name and body. If the boolean flag is set
     to true, then this is a local redefinition. *)
@@ -68,7 +67,7 @@ val interp_ltac : KerName.t -> glob_tactic_expr
 val is_ltac_for_ml_tactic : KerName.t -> bool
 (** Whether the tactic is defined from ML-side *)
 
-val tac_deprecation : KerName.t -> deprecation option
+val tac_deprecation : KerName.t -> Deprecation.t option
 (** The tactic deprecation notice, if any *)
 
 type ltac_entry = {
@@ -78,7 +77,7 @@ type ltac_entry = {
   (** The current body of the tactic *)
   tac_redef : ModPath.t list;
   (** List of modules redefining the tactic in reverse chronological order *)
-  tac_deprecation : deprecation option;
+  tac_deprecation : Deprecation.t option;
   (** Deprecation notice to be printed when the tactic is used *)
 }
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index c1f7fab123..7434f81946 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -119,18 +119,13 @@ let intern_constr_reference strict ist qid =
 (* Internalize an isolated reference in position of tactic *)
 
 let warn_deprecated_tactic =
-  CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated"
-    (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++
-      strbrk " is deprecated" ++
-      pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
-      str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
+  Deprecation.create_warning ~object_name:"Tactic" ~warning_name:"deprecated-tactic"
+    pr_qualid
 
 let warn_deprecated_alias =
-  CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated"
-    (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++
-      strbrk " is deprecated since" ++
-      pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
-      str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
+  Deprecation.create_warning ~object_name:"Tactic Notation"
+    ~warning_name:"deprecated-tactic-notation"
+    Pptactic.pr_alias_key
 
 let intern_isolated_global_tactic_reference qid =
   let loc = qid.CAst.loc in