Skip to content

Removed unused deprecation arguments in tacentries #21876

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coqbot-app merged 1 commit into from
Apr 7, 2026
+6 −6
Merged

Removed unused deprecation arguments in tacentries #21876

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion plugins/ltac/g_ltac.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 4 additions & 4 deletions plugins/ltac/tacentries.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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 *)
Expand Down Expand Up @@ -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;
}
Expand Down
2 changes: 1 addition & 1 deletion plugins/ltac/tacentries.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading