Removed unused deprecation arguments in tacentries

Deprecation is handled in Interp not Synterp

Author: SkySkimmer

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

@@ -334,7 +334,7 @@ let add_glob_tactic_notation ?deprecation tacobj ids tac =
     { alias_args = ids; alias_body = tac; alias_deprecation = deprecation } 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;
@@ -353,9 +353,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                                                  *)
@@ -409,7 +409,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 }
   in
   let for_interp = List.mapi map (List.rev prods) in

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