Merge PR #7907: Tactic deprecation machinery

15 files changed, 166 insertions, 56 deletions

diff --git a/CHANGES b/CHANGES
index 6dce7b0db..fdd4feb59 100644
--- a/CHANGES
+++ b/CHANGES
@@ -38,6 +38,8 @@ Tactics
   without adding new ones. Preexisting tactic `constr_eq_nounivs` can
   still be used if you really want to ignore universe constraints.
 
+- Tactics and tactic notations now understand the `deprecated` attribute.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index ac6a20198..8250b4b3d 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1430,6 +1430,12 @@ the following attributes names are recognized:
     Takes as value the optional attributes ``since`` and ``note``;
     both have a string value.
 
+    This attribute can trigger the following warnings:
+
+    .. warn:: Tactic @qualid is deprecated since @string. @string.
+
+    .. warn:: Tactic Notation @qualid is deprecated since @string. @string.
+
 Here are a few examples:
 
 .. coqtop:: all reset
@@ -1440,7 +1446,7 @@ Here are a few examples:
           exact O.
         Defined.
 
-        #[deprecated(since="8.9.0", note="use idtac instead")]
+        #[deprecated(since="8.9.0", note="Use idtac instead.")]
         Ltac foo := idtac.
 
         Goal True.
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index cea0bed59..02da61ef7 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -49,13 +49,17 @@ EXTEND
   GLOBAL: str_item;
   str_item:
     [ [ "TACTIC"; "EXTEND"; s = tac_name;
+        depr = OPT [ "DEPRECATED"; depr = LIDENT -> depr ];
         level = OPT [ "AT"; UIDENT "LEVEL"; level = INT -> level ];
         OPT "|"; l = LIST1 tacrule SEP "|";
         "END" ->
         let level = match level with Some i -> int_of_string i | None -> 0 in
         let level = mlexpr_of_int level in
+        let depr = mlexpr_of_option (fun l -> <:expr< $lid:l$ >>) depr in
         let l = <:expr< Tacentries.($mlexpr_of_list (fun x -> x) l$) >> in
-        declare_str_items loc [ <:str_item< Tacentries.tactic_extend $plugin_name$ $str:s$ ~{ level = $level$ } $l$ >> ] ] ]
+        declare_str_items loc [ <:str_item< Tacentries.tactic_extend
+          $plugin_name$ $str:s$ ~{ level = $level$ } ?{ deprecation =
+          $depr$ } $l$ >> ] ] ]
   ;
   tacrule:
     [ [ "["; l = LIST1 tacargs; "]";
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 9d86f21d4..c13bd69da 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -287,12 +287,14 @@ GEXTEND Gram
 
   (* Definitions for tactics *)
   tacdef_body:
-    [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr ->
+    [ [ name = Constr.global; it=LIST1 input_fun;
+        redef = ltac_def_kind; body = tactic_expr ->
           if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body))
           else
             let id = reference_to_id name in
             Tacexpr.TacticDefinition (id, TacFun (it, body))
-      | name = Constr.global; redef = ltac_def_kind; body = tactic_expr ->
+      | name = Constr.global; redef = ltac_def_kind;
+        body = tactic_expr ->
           if redef then Tacexpr.TacticRedefinition (name, body)
           else
             let id = reference_to_id name in
@@ -468,7 +470,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation
   [ VtSideff [], VtNow ] ->
   [ fun ~atts ~st -> let open Vernacinterp in
       let n = Option.default 0 n in
-      Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e;
+      let deprecation = atts.deprecated in
+      Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e;
       st
   ]
 END
@@ -512,7 +515,8 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
       | TacticDefinition ({CAst.v=r},_) -> r
       | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
   ] -> [ fun ~atts ~st -> let open Vernacinterp in
-           Tacentries.register_ltac (Locality.make_module_locality atts.locality) l;
+           let deprecation = atts.deprecated in
+           Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
            st
   ]
 END
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fac464a62..4b834d66d 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -252,7 +252,7 @@ type tactic_grammar_obj = {
   tacobj_key : KerName.t;
   tacobj_local : locality_flag;
   tacobj_tacgram : tactic_grammar;
-  tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
+  tacobj_body : Tacenv.alias_tactic;
   tacobj_forml : bool;
 }
 
@@ -288,10 +288,11 @@ let load_tactic_notation i (_, tobj) =
     extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
 
 let subst_tactic_notation (subst, tobj) =
-  let (ids, body) = tobj.tacobj_body in
+  let open Tacenv in
+  let alias = tobj.tacobj_body in
   { tobj with
     tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
-    tacobj_body = (ids, Tacsubst.subst_tactic subst body);
+    tacobj_body = { alias with alias_body = Tacsubst.subst_tactic subst alias.alias_body };
   }
 
 let classify_tactic_notation tacobj = Substitute tacobj
@@ -308,25 +309,26 @@ let cons_production_parameter = function
 | TacTerm _ -> None
 | TacNonTerm (_, (_, ido)) -> ido
 
-let add_glob_tactic_notation local ~level prods forml ids tac =
+let add_glob_tactic_notation local ~level ?deprecation prods forml ids tac =
   let parule = {
     tacgram_level = level;
     tacgram_prods = prods;
   } in
+  let open Tacenv in
   let tacobj = {
     tacobj_key = make_fresh_key prods;
     tacobj_local = local;
     tacobj_tacgram = parule;
-    tacobj_body = (ids, tac);
+    tacobj_body = { alias_args = ids; alias_body = tac; alias_deprecation = deprecation };
     tacobj_forml = forml;
   } in
   Lib.add_anonymous_leaf (inTacticGrammar tacobj)
 
-let add_tactic_notation local n prods e =
+let add_tactic_notation local n ?deprecation prods e =
   let ids = List.map_filter cons_production_parameter prods in
   let prods = List.map interp_prod_item prods in
   let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
-  add_glob_tactic_notation local ~level:n prods false ids tac
+  add_glob_tactic_notation local ~level:n ?deprecation prods false ids tac
 
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
@@ -366,7 +368,7 @@ let extend_atomic_tactic name entries =
   in
   List.iteri add_atomic entries
 
-let add_ml_tactic_notation name ~level prods =
+let add_ml_tactic_notation name ~level ?deprecation prods =
   let len = List.length prods in
   let iter i prods =
     let open Tacexpr in
@@ -378,7 +380,7 @@ let add_ml_tactic_notation name ~level prods =
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
     let map id = Reference (Locus.ArgVar (CAst.make id)) in
     let tac = TacML (Loc.tag (entry, List.map map ids)) in
-    add_glob_tactic_notation false ~level prods true ids tac
+    add_glob_tactic_notation false ~level ?deprecation prods true ids tac
   in
   List.iteri iter (List.rev prods);
   (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
@@ -430,7 +432,7 @@ let warn_unusable_identifier =
       (fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++
         strbrk "may be unusable because of a conflict with a notation.")
 
-let register_ltac local tacl =
+let register_ltac local ?deprecation tacl =
   let map tactic_body =
     match tactic_body with
     | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
@@ -483,10 +485,10 @@ let register_ltac local tacl =
   let defs = States.with_state_protection defs () in
   let iter (def, tac) = match def with
   | NewTac id ->
-    Tacenv.register_ltac false local id tac;
+    Tacenv.register_ltac false local id tac ?deprecation;
     Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
   | UpdateTac kn ->
-    Tacenv.redefine_ltac local kn tac;
+    Tacenv.redefine_ltac local kn tac ?deprecation;
     let name = Tacenv.shortest_qualid_of_tactic kn in
     Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
   in
@@ -658,7 +660,7 @@ let lift_constr_tac_to_ml_tac vars tac =
   end in
   tac
 
-let tactic_extend plugin_name tacname ~level sign =
+let tactic_extend plugin_name tacname ~level ?deprecation sign =
   let open Tacexpr in
   let ml_tactic_name =
     { mltac_tactic = tacname;
@@ -687,10 +689,10 @@ let tactic_extend plugin_name tacname ~level sign =
       This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
     let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
     let id = Names.Id.of_string name in
-    let obj () = Tacenv.register_ltac true false id body in
+    let obj () = Tacenv.register_ltac true false id body ?deprecation in
     let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
     Mltop.declare_cache_obj obj plugin_name
   | _ ->
-  let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in
+  let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in
   Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
   Mltop.declare_cache_obj obj plugin_name
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index f873631ff..138a584e0 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
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index d5ab2d690..0bb9ccb1d 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -52,7 +52,11 @@ let shortest_qualid_of_tactic kn =
 (** Tactic notations (TacAlias) *)
 
 type alias = KerName.t
-type alias_tactic = Id.t list * glob_tactic_expr
+type alias_tactic =
+  { alias_args: Id.t list;
+    alias_body: glob_tactic_expr;
+    alias_deprecation: Vernacinterp.deprecation option;
+  }
 
 let alias_map = Summary.ref ~name:"tactic-alias"
   (KNmap.empty : alias_tactic KNmap.t)
@@ -118,6 +122,7 @@ type ltac_entry = {
   tac_for_ml : bool;
   tac_body : glob_tactic_expr;
   tac_redef : ModPath.t list;
+  tac_deprecation : Vernacinterp.deprecation option
 }
 
 let mactab =
@@ -130,8 +135,12 @@ let interp_ltac r = (KNmap.find r !mactab).tac_body
 
 let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml
 
-let add kn b t =
-  let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in
+let add ~deprecation kn b t =
+  let entry = { tac_for_ml = b;
+                tac_body = t;
+                tac_redef = [];
+                tac_deprecation = deprecation;
+              } in
   mactab := KNmap.add kn entry !mactab
 
 let replace kn path t =
@@ -139,34 +148,38 @@ let replace kn path t =
   let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
   mactab := KNmap.modify kn entry !mactab
 
-let load_md i ((sp, kn), (local, id, b, t)) = match id with
+let tac_deprecation kn =
+  try (KNmap.find kn !mactab).tac_deprecation with Not_found -> None
+
+let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
 | None ->
   let () = if not local then push_tactic (Until i) sp kn in
-  add kn b t
+  add ~deprecation kn b t
 | Some kn0 -> replace kn0 kn t
 
-let open_md i ((sp, kn), (local, id, b, t)) = match id with
+let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
 | None ->
   let () = if not local then push_tactic (Exactly i) sp kn in
-  add kn b t
+  add ~deprecation kn b t
 | Some kn0 -> replace kn0 kn t
 
-let cache_md ((sp, kn), (local, id ,b, t)) = match id with
+let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with
 | None ->
   let () = push_tactic (Until 1) sp kn in
-  add kn b t
+  add ~deprecation kn b t
 | Some kn0 -> replace kn0 kn t
 
 let subst_kind subst id = match id with
 | None -> None
 | Some kn -> Some (Mod_subst.subst_kn subst kn)
 
-let subst_md (subst, (local, id, b, t)) =
-  (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t)
+let subst_md (subst, (local, id, b, t, deprecation)) =
+  (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t, deprecation)
 
-let classify_md (local, _, _, _ as o) = Substitute o
+let classify_md (local, _, _, _, _ as o) = Substitute o
 
-let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
+let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
+           Vernacinterp.deprecation option -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
@@ -174,8 +187,8 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
      subst_function = subst_md;
      classify_function = classify_md}
 
-let register_ltac for_ml local id tac =
-  ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac)))
+let register_ltac for_ml local ?deprecation id tac =
+  ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac, deprecation)))
 
-let redefine_ltac local kn tac =
-  Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac))
+let redefine_ltac local ?deprecation kn tac =
+  Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac, deprecation))
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 3af2f2a46..7143f5185 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,6 +12,7 @@ open Names
 open Libnames
 open Tacexpr
 open Geninterp
+open Vernacinterp
 
 (** This module centralizes the various ways of registering tactics. *)
 
@@ -29,7 +30,11 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid
 type alias = KerName.t
 (** Type of tactic alias, used in the [TacAlias] node. *)
 
-type alias_tactic = Id.t list * glob_tactic_expr
+type alias_tactic =
+  { alias_args: Id.t list;
+    alias_body: glob_tactic_expr;
+    alias_deprecation: Vernacinterp.deprecation option;
+  }
 (** Contents of a tactic notation *)
 
 val register_alias : alias -> alias_tactic -> unit
@@ -43,7 +48,8 @@ val check_alias : alias -> bool
 
 (** {5 Coq tactic definitions} *)
 
-val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
+val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t ->
+  glob_tactic_expr -> unit
 (** Register a new Ltac with the given name and body.
 
     The first boolean indicates whether this is done from ML side, rather than
@@ -51,7 +57,8 @@ val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
     definition. It also puts the Ltac name in the nametab, so that it can be
     used unqualified. *)
 
-val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit
+val redefine_ltac : bool -> ?deprecation:deprecation -> 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. *)
 
@@ -61,6 +68,9 @@ 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
+(** The tactic deprecation notice, if any *)
+
 type ltac_entry = {
   tac_for_ml : bool;
   (** Whether the tactic is defined from ML-side *)
@@ -68,6 +78,8 @@ 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;
+  (** Deprecation notice to be printed when the tactic is used *)
 }
 
 val ltac_entries : unit -> ltac_entry KNmap.t
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 06d2711ad..59b748e25 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -398,5 +398,5 @@ type ltac_call_kind =
 type ltac_trace = ltac_call_kind Loc.located list
 
 type tacdef_body =
-  | TacticDefinition of lident * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
-  | TacticRedefinition of qualid * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
+  | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+  | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 71e1edfd7..3a0badb28 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -398,5 +398,5 @@ type ltac_call_kind =
 type ltac_trace = ltac_call_kind Loc.located list
 
 type tacdef_body =
-  | TacticDefinition of lident * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
-  | TacticRedefinition of qualid * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
+  | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+  | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 481fc30df..144480062 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -117,9 +117,26 @@ 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.Vernacinterp.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+
+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.Vernacinterp.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+
 let intern_isolated_global_tactic_reference qid =
   let loc = qid.CAst.loc in
-  TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
+  let kn = Tacenv.locate_tactic qid in
+  Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
+    Tacenv.tac_deprecation kn;
+  TacCall (Loc.tag ?loc (ArgArg (loc,kn),[]))
 
 let intern_isolated_tactic_reference strict ist qid =
   (* An ltac reference *)
@@ -137,7 +154,11 @@ let intern_isolated_tactic_reference strict ist qid =
 (* Internalize an applied tactic reference *)
 
 let intern_applied_global_tactic_reference qid =
-  ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid)
+  let loc = qid.CAst.loc in
+  let kn = Tacenv.locate_tactic qid in
+  Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
+    Tacenv.tac_deprecation kn;
+  ArgArg (loc,kn)
 
 let intern_applied_tactic_reference ist qid =
   (* An ltac reference *)
@@ -643,6 +664,8 @@ and intern_tactic_seq onlytac ist = function
 
   (* For extensions *)
   | TacAlias (loc,(s,l)) ->
+      let alias = Tacenv.interp_alias s in
+      Option.iter (fun o -> warn_deprecated_alias ?loc (s,o)) @@ alias.Tacenv.alias_deprecation;
       let l = List.map (intern_tacarg !strict_check false ist) l in
       ist.ltacvars, TacAlias (Loc.tag ?loc (s,l))
   | TacML (loc,(opn,l)) ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d9ac96d89..77b5b06d4 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: \
diff --git a/test-suite/output/Deprecation.out b/test-suite/output/Deprecation.out
new file mode 100644
index 000000000..7e290847c
--- /dev/null
+++ b/test-suite/output/Deprecation.out
@@ -0,0 +1,3 @@
+File "stdin", line 5, characters 0-3:
+Warning: Tactic foo is deprecated since X.Y. Use idtac instead.
+[deprecated-tactic,deprecated]
diff --git a/test-suite/output/Deprecation.v b/test-suite/output/Deprecation.v
new file mode 100644
index 000000000..04d5eb3d4
--- /dev/null
+++ b/test-suite/output/Deprecation.v
@@ -0,0 +1,6 @@
+#[deprecated(since = "X.Y", note = "Use idtac instead.")]
+ Ltac foo := idtac.
+
+Goal True.
+foo.
+Abort.
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.