1 files changed, 31 insertions, 18 deletions

diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index d5ab2d69..1f2c722b 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,43 +135,51 @@ 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 =
-  let (path, _, _) = KerName.repr path in
+  let path = KerName.modpath path in
   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))