diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 3e158f651c6f..2267b7579996 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -423,7 +423,7 @@ VERNAC COMMAND EXTEND VernacTacticNotation
   { VtSideff ([], VtNow) } SYNTERP AS tacobj {
     let n = Option.default 0 n in
     let local = Locality.make_module_locality locality in
-    Tacentries.add_tactic_notation_syntax local n ?deprecation r
+    Tacentries.add_tactic_notation_syntax local n r
   } ->
   {
     Tacentries.add_tactic_notation ?deprecation tacobj e
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 8b28a88024bc..8119414ebae1 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -337,7 +337,7 @@ let add_glob_tactic_notation ?deprecation tacobj ids tac =
   in
   Lib.add_leaf (inTacticGrammar (tacobj, body))
 
-let add_glob_tactic_notation_syntax local ~level ?deprecation prods forml =
+let add_glob_tactic_notation_syntax local ~level prods forml =
   let parule = {
     tacgram_level = level;
     tacgram_prods = prods;
@@ -356,9 +356,9 @@ let add_tactic_notation ?deprecation tacobj e =
   let tac = Tacintern.glob_tactic_env ids (Global.env()) UnivNames.empty_binders e in
   add_glob_tactic_notation ?deprecation tacobj ids tac
 
-let add_tactic_notation_syntax local n ?deprecation prods =
+let add_tactic_notation_syntax local n prods =
   let prods = List.map interp_prod_item prods in
-  add_glob_tactic_notation_syntax local ~level:n ?deprecation prods false
+  add_glob_tactic_notation_syntax local ~level:n prods false
 
 (**********************************************************************)
 (* ML Tactic entries                                                  *)
@@ -412,7 +412,7 @@ let synterp_add_ml_tactic_notation name ~level ?deprecation prods =
     let entry = { mltac_name = name; mltac_index = len - i - 1 } in
     let map id = Reference (Locus.ArgVar (CAst.make id)) in
     let tac = CAst.make (TacML (entry, List.map map ids)) in
-    let tacobj = add_glob_tactic_notation_syntax false ~level ?deprecation prods true in
+    let tacobj = add_glob_tactic_notation_syntax false ~level prods true in
     tacobj, { Tacenv.alias_args = ids; alias_body = tac; alias_deprecation = deprecation;
               alias_is_ml = Some entry;
             }
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 7afc5483b6b3..aa31a8f38e8b 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -43,7 +43,7 @@ val add_tactic_notation :
     productions [prods] and returning the body [expr] *)
 
 val add_tactic_notation_syntax :
-  locality_flag -> int -> ?deprecation:Deprecation.t -> raw_argument
+  locality_flag -> int -> raw_argument
   grammar_tactic_prod_item_expr list ->
   tactic_grammar_obj