Merge PR #21876: Removed unused deprecation arguments in tacentries

Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>

Author: coqbot-app[bot]

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

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;
             }

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