1 files changed, 10 insertions, 6 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 620f14707..c13bd69da 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -46,10 +46,10 @@ let reference_to_id qid =
     CErrors.user_err ?loc:qid.CAst.loc
       (str "This expression should be a simple identifier.")
 
-let tactic_mode = Gram.entry_create "vernac:tactic_command"
+let tactic_mode = Entry.create "vernac:tactic_command"
 
 let new_entry name =
-  let e = Gram.entry_create name in
+  let e = Entry.create name in
   e
 
 let toplevel_selector = new_entry "vernac:toplevel_selector"
@@ -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