`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.

1 files changed, 5 insertions, 6 deletions

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 *)
 }