aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extraargs.ml439
-rw-r--r--plugins/ltac/extraargs.mli16
-rw-r--r--plugins/ltac/extratactics.ml419
-rw-r--r--plugins/ltac/g_ltac.ml416
-rw-r--r--plugins/ltac/pltac.ml9
-rw-r--r--plugins/ltac/pltac.mli38
-rw-r--r--plugins/ltac/tacentries.ml32
-rw-r--r--plugins/ltac/tacentries.mli15
-rw-r--r--plugins/ltac/tacenv.ml47
-rw-r--r--plugins/ltac/tacenv.mli18
-rw-r--r--plugins/ltac/tacexpr.ml4
-rw-r--r--plugins/ltac/tacexpr.mli4
-rw-r--r--plugins/ltac/tacintern.ml27
-rw-r--r--plugins/ltac/tacinterp.ml8
14 files changed, 160 insertions, 132 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index dae2582bd..dbbdbfa39 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -297,25 +297,6 @@ END
(* spiwack: the print functions are incomplete, but I don't know what they are
used for *)
-let pr_r_nat_field natf =
- str "nat " ++
- match natf with
- | Retroknowledge.NatType -> str "type"
- | Retroknowledge.NatPlus -> str "plus"
- | Retroknowledge.NatTimes -> str "times"
-
-let pr_r_n_field nf =
- str "binary N " ++
- match nf with
- | Retroknowledge.NPositive -> str "positive"
- | Retroknowledge.NType -> str "type"
- | Retroknowledge.NTwice -> str "twice"
- | Retroknowledge.NTwicePlusOne -> str "twice plus one"
- | Retroknowledge.NPhi -> str "phi"
- | Retroknowledge.NPhiInv -> str "phi inv"
- | Retroknowledge.NPlus -> str "plus"
- | Retroknowledge.NTimes -> str "times"
-
let pr_r_int31_field i31f =
str "int31 " ++
match i31f with
@@ -353,26 +334,6 @@ let pr_retroknowledge_field f =
| Retroknowledge.KInt31 (group, i31f) -> (pr_r_int31_field i31f) ++
spc () ++ str "in " ++ qs group
-VERNAC ARGUMENT EXTEND retroknowledge_nat
-PRINTED BY pr_r_nat_field
-| [ "nat" "type" ] -> [ Retroknowledge.NatType ]
-| [ "nat" "plus" ] -> [ Retroknowledge.NatPlus ]
-| [ "nat" "times" ] -> [ Retroknowledge.NatTimes ]
-END
-
-
-VERNAC ARGUMENT EXTEND retroknowledge_binary_n
-PRINTED BY pr_r_n_field
-| [ "binary" "N" "positive" ] -> [ Retroknowledge.NPositive ]
-| [ "binary" "N" "type" ] -> [ Retroknowledge.NType ]
-| [ "binary" "N" "twice" ] -> [ Retroknowledge.NTwice ]
-| [ "binary" "N" "twice" "plus" "one" ] -> [ Retroknowledge.NTwicePlusOne ]
-| [ "binary" "N" "phi" ] -> [ Retroknowledge.NPhi ]
-| [ "binary" "N" "phi" "inv" ] -> [ Retroknowledge.NPhiInv ]
-| [ "binary" "N" "plus" ] -> [ Retroknowledge.NPlus ]
-| [ "binary" "N" "times" ] -> [ Retroknowledge.NTimes ]
-END
-
VERNAC ARGUMENT EXTEND retroknowledge_int31
PRINTED BY pr_r_int31_field
| [ "int31" "bits" ] -> [ Retroknowledge.Int31Bits ]
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 737147884..e477b12cd 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -14,12 +14,12 @@ open Constrexpr
open Glob_term
val wit_orient : bool Genarg.uniform_genarg_type
-val orient : bool Pcoq.Gram.entry
+val orient : bool Pcoq.Entry.t
val pr_orient : bool -> Pp.t
val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
-val occurrences : (int list Locus.or_var) Pcoq.Gram.entry
+val occurrences : (int list Locus.or_var) Pcoq.Entry.t
val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type
val pr_occurrences : int list Locus.or_var -> Pp.t
val occurrences_of : int list -> Locus.occurrences
@@ -46,8 +46,8 @@ val wit_casted_constr :
Tacexpr.glob_constr_and_expr,
EConstr.t) Genarg.genarg_type
-val glob : constr_expr Pcoq.Gram.entry
-val lglob : constr_expr Pcoq.Gram.entry
+val glob : constr_expr Pcoq.Entry.t
+val lglob : constr_expr Pcoq.Entry.t
type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
@@ -55,10 +55,10 @@ type loc_place = lident gen_place
type place = Id.t gen_place
val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
-val hloc : loc_place Pcoq.Gram.entry
+val hloc : loc_place Pcoq.Entry.t
val pr_hloc : loc_place -> Pp.t
-val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
+val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Entry.t
val wit_by_arg_tac :
(raw_tactic_expr option,
glob_tactic_expr option,
@@ -68,13 +68,13 @@ val pr_by_arg_tac :
(int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
raw_tactic_expr option -> Pp.t
-val test_lpar_id_colon : unit Pcoq.Gram.entry
+val test_lpar_id_colon : unit Pcoq.Entry.t
val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
(** Spiwack: Primitive for retroknowledge registration *)
-val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
+val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t
val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
val wit_in_clause :
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index f24ab2bdd..dc027c404 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -604,8 +604,11 @@ let subst_var_with_hole occ tid t =
else
(incr locref;
DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
- GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
- IntroAnonymous, None)))
+ GHole (Evar_kinds.QuestionMark {
+ Evar_kinds.qm_obligation=Evar_kinds.Define true;
+ Evar_kinds.qm_name=Anonymous;
+ Evar_kinds.qm_record_field=None;
+ }, IntroAnonymous, None)))
else x
| _ -> map_glob_constr_left_to_right substrec x in
let t' = substrec t
@@ -616,13 +619,21 @@ let subst_hole_with_term occ tc t =
let locref = ref 0 in
let occref = ref occ in
let rec substrec c = match DAst.get c with
- | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s) ->
+ | GHole (Evar_kinds.QuestionMark {
+ Evar_kinds.qm_obligation=Evar_kinds.Define true;
+ Evar_kinds.qm_name=Anonymous;
+ Evar_kinds.qm_record_field=None;
+ }, IntroAnonymous, s) ->
decr occref;
if Int.equal !occref 0 then tc
else
(incr locref;
DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
- GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),IntroAnonymous,s))
+ GHole (Evar_kinds.QuestionMark {
+ Evar_kinds.qm_obligation=Evar_kinds.Define true;
+ Evar_kinds.qm_name=Anonymous;
+ Evar_kinds.qm_record_field=None;
+ },IntroAnonymous,s))
| _ -> map_glob_constr_left_to_right substrec c
in
substrec t
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
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index e9711268c..759bb62fd 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -11,11 +11,10 @@
open Pcoq
(* Main entry for extensions *)
-let simple_tactic = Gram.entry_create "tactic:simple_tactic"
+let simple_tactic = Entry.create "tactic:simple_tactic"
-let make_gen_entry _ name = Gram.entry_create ("tactic:" ^ name)
+let make_gen_entry _ name = Entry.create ("tactic:" ^ name)
-(* Entries that can be referred via the string -> Gram.entry table *)
(* Typically for tactic user extensions *)
let open_constr =
make_gen_entry utactic "open_constr"
@@ -23,7 +22,7 @@ let constr_with_bindings =
make_gen_entry utactic "constr_with_bindings"
let bindings =
make_gen_entry utactic "bindings"
-let hypident = Gram.entry_create "hypident"
+let hypident = Entry.create "hypident"
let constr_may_eval = make_gen_entry utactic "constr_may_eval"
let constr_eval = make_gen_entry utactic "constr_eval"
let uconstr =
@@ -40,7 +39,7 @@ let clause_dft_concl =
(* Main entries for ltac *)
-let tactic_arg = Gram.entry_create "tactic:tactic_arg"
+let tactic_arg = Entry.create "tactic:tactic_arg"
let tactic_expr = make_gen_entry utactic "tactic_expr"
let binder_tactic = make_gen_entry utactic "binder_tactic"
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index c5aa542fd..9bff98b6c 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -17,22 +17,22 @@ open Tacexpr
open Genredexpr
open Tactypes
-val open_constr : constr_expr Gram.entry
-val constr_with_bindings : constr_expr with_bindings Gram.entry
-val bindings : constr_expr bindings Gram.entry
-val hypident : (Names.lident * Locus.hyp_location_flag) Gram.entry
-val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
-val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry
-val uconstr : constr_expr Gram.entry
-val quantified_hypothesis : quantified_hypothesis Gram.entry
-val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry
-val int_or_var : int Locus.or_var Gram.entry
-val simple_tactic : raw_tactic_expr Gram.entry
-val simple_intropattern : constr_expr intro_pattern_expr CAst.t Gram.entry
-val in_clause : Names.lident Locus.clause_expr Gram.entry
-val clause_dft_concl : Names.lident Locus.clause_expr Gram.entry
-val tactic_arg : raw_tactic_arg Gram.entry
-val tactic_expr : raw_tactic_expr Gram.entry
-val binder_tactic : raw_tactic_expr Gram.entry
-val tactic : raw_tactic_expr Gram.entry
-val tactic_eoi : raw_tactic_expr Gram.entry
+val open_constr : constr_expr Entry.t
+val constr_with_bindings : constr_expr with_bindings Entry.t
+val bindings : constr_expr bindings Entry.t
+val hypident : (Names.lident * Locus.hyp_location_flag) Entry.t
+val constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t
+val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Entry.t
+val uconstr : constr_expr Entry.t
+val quantified_hypothesis : quantified_hypothesis Entry.t
+val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Entry.t
+val int_or_var : int Locus.or_var Entry.t
+val simple_tactic : raw_tactic_expr Entry.t
+val simple_intropattern : constr_expr intro_pattern_expr CAst.t Entry.t
+val in_clause : Names.lident Locus.clause_expr Entry.t
+val clause_dft_concl : Names.lident Locus.clause_expr Entry.t
+val tactic_arg : raw_tactic_arg Entry.t
+val tactic_expr : raw_tactic_expr Entry.t
+val binder_tactic : raw_tactic_expr Entry.t
+val tactic : raw_tactic_expr Entry.t
+val tactic_eoi : raw_tactic_expr Entry.t
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fac464a62..4b834d66d 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -252,7 +252,7 @@ type tactic_grammar_obj = {
tacobj_key : KerName.t;
tacobj_local : locality_flag;
tacobj_tacgram : tactic_grammar;
- tacobj_body : Id.t list * Tacexpr.glob_tactic_expr;
+ tacobj_body : Tacenv.alias_tactic;
tacobj_forml : bool;
}
@@ -288,10 +288,11 @@ let load_tactic_notation i (_, tobj) =
extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram
let subst_tactic_notation (subst, tobj) =
- let (ids, body) = tobj.tacobj_body in
+ let open Tacenv in
+ let alias = tobj.tacobj_body in
{ tobj with
tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key;
- tacobj_body = (ids, Tacsubst.subst_tactic subst body);
+ tacobj_body = { alias with alias_body = Tacsubst.subst_tactic subst alias.alias_body };
}
let classify_tactic_notation tacobj = Substitute tacobj
@@ -308,25 +309,26 @@ let cons_production_parameter = function
| TacTerm _ -> None
| TacNonTerm (_, (_, ido)) -> ido
-let add_glob_tactic_notation local ~level prods forml ids tac =
+let add_glob_tactic_notation local ~level ?deprecation prods forml ids tac =
let parule = {
tacgram_level = level;
tacgram_prods = prods;
} in
+ let open Tacenv in
let tacobj = {
tacobj_key = make_fresh_key prods;
tacobj_local = local;
tacobj_tacgram = parule;
- tacobj_body = (ids, tac);
+ tacobj_body = { alias_args = ids; alias_body = tac; alias_deprecation = deprecation };
tacobj_forml = forml;
} in
Lib.add_anonymous_leaf (inTacticGrammar tacobj)
-let add_tactic_notation local n prods e =
+let add_tactic_notation local n ?deprecation prods e =
let ids = List.map_filter cons_production_parameter prods in
let prods = List.map interp_prod_item prods in
let tac = Tacintern.glob_tactic_env ids (Global.env()) e in
- add_glob_tactic_notation local ~level:n prods false ids tac
+ add_glob_tactic_notation local ~level:n ?deprecation prods false ids tac
(**********************************************************************)
(* ML Tactic entries *)
@@ -366,7 +368,7 @@ let extend_atomic_tactic name entries =
in
List.iteri add_atomic entries
-let add_ml_tactic_notation name ~level prods =
+let add_ml_tactic_notation name ~level ?deprecation prods =
let len = List.length prods in
let iter i prods =
let open Tacexpr in
@@ -378,7 +380,7 @@ let add_ml_tactic_notation name ~level prods =
let entry = { mltac_name = name; mltac_index = len - i - 1 } in
let map id = Reference (Locus.ArgVar (CAst.make id)) in
let tac = TacML (Loc.tag (entry, List.map map ids)) in
- add_glob_tactic_notation false ~level prods true ids tac
+ add_glob_tactic_notation false ~level ?deprecation prods true ids tac
in
List.iteri iter (List.rev prods);
(** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
@@ -430,7 +432,7 @@ let warn_unusable_identifier =
(fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++
strbrk "may be unusable because of a conflict with a notation.")
-let register_ltac local tacl =
+let register_ltac local ?deprecation tacl =
let map tactic_body =
match tactic_body with
| Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
@@ -483,10 +485,10 @@ let register_ltac local tacl =
let defs = States.with_state_protection defs () in
let iter (def, tac) = match def with
| NewTac id ->
- Tacenv.register_ltac false local id tac;
+ Tacenv.register_ltac false local id tac ?deprecation;
Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
| UpdateTac kn ->
- Tacenv.redefine_ltac local kn tac;
+ Tacenv.redefine_ltac local kn tac ?deprecation;
let name = Tacenv.shortest_qualid_of_tactic kn in
Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined")
in
@@ -658,7 +660,7 @@ let lift_constr_tac_to_ml_tac vars tac =
end in
tac
-let tactic_extend plugin_name tacname ~level sign =
+let tactic_extend plugin_name tacname ~level ?deprecation sign =
let open Tacexpr in
let ml_tactic_name =
{ mltac_tactic = tacname;
@@ -687,10 +689,10 @@ let tactic_extend plugin_name tacname ~level sign =
This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
let id = Names.Id.of_string name in
- let obj () = Tacenv.register_ltac true false id body in
+ let obj () = Tacenv.register_ltac true false id body ?deprecation in
let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
Mltop.declare_cache_obj obj plugin_name
| _ ->
- let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in
+ let obj () = add_ml_tactic_notation ml_tactic_name ~level ?deprecation (List.map clause_of_ty_ml sign) in
Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
Mltop.declare_cache_obj obj plugin_name
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 9bba9ba71..138a584e0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,10 +12,12 @@
open Vernacexpr
open Tacexpr
+open Vernacinterp
(** {5 Tactic Definitions} *)
-val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
+val register_ltac : locality_flag -> ?deprecation:deprecation ->
+ Tacexpr.tacdef_body list -> unit
(** Adds new Ltac definitions to the environment. *)
(** {5 Tactic Notations} *)
@@ -34,8 +36,8 @@ type argument = Genarg.ArgT.any Extend.user_symbol
leaves. *)
val add_tactic_notation :
- locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list ->
- raw_tactic_expr -> unit
+ locality_flag -> int -> ?deprecation:deprecation -> raw_argument
+ grammar_tactic_prod_item_expr list -> raw_tactic_expr -> unit
(** [add_tactic_notation local level prods expr] adds a tactic notation in the
environment at level [level] with locality [local] made of the grammar
productions [prods] and returning the body [expr] *)
@@ -47,7 +49,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -
to finding an argument by name (as in {!Genarg}) if there is none
matching. *)
-val add_ml_tactic_notation : ml_tactic_name -> level:int ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int -> ?deprecation:deprecation ->
argument grammar_tactic_prod_item_expr list list -> unit
(** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
ML-side macro. *)
@@ -55,7 +57,7 @@ val add_ml_tactic_notation : ml_tactic_name -> level:int ->
(** {5 Tactic Quotations} *)
val create_ltac_quotation : string ->
- ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit
+ ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Entry.t * int option) -> unit
(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is,
Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and
generates an argument using [f] on the entry parsed by [e]. *)
@@ -78,4 +80,5 @@ type _ ty_sig =
type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
-val tactic_extend : string -> string -> level:Int.t -> ty_ml list -> unit
+val tactic_extend : string -> string -> level:Int.t ->
+ ?deprecation:deprecation -> ty_ml list -> unit
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index d5ab2d690..0bb9ccb1d 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -52,7 +52,11 @@ let shortest_qualid_of_tactic kn =
(** Tactic notations (TacAlias) *)
type alias = KerName.t
-type alias_tactic = Id.t list * glob_tactic_expr
+type alias_tactic =
+ { alias_args: Id.t list;
+ alias_body: glob_tactic_expr;
+ alias_deprecation: Vernacinterp.deprecation option;
+ }
let alias_map = Summary.ref ~name:"tactic-alias"
(KNmap.empty : alias_tactic KNmap.t)
@@ -118,6 +122,7 @@ type ltac_entry = {
tac_for_ml : bool;
tac_body : glob_tactic_expr;
tac_redef : ModPath.t list;
+ tac_deprecation : Vernacinterp.deprecation option
}
let mactab =
@@ -130,8 +135,12 @@ let interp_ltac r = (KNmap.find r !mactab).tac_body
let is_ltac_for_ml_tactic r = (KNmap.find r !mactab).tac_for_ml
-let add kn b t =
- let entry = { tac_for_ml = b; tac_body = t; tac_redef = [] } in
+let add ~deprecation kn b t =
+ let entry = { tac_for_ml = b;
+ tac_body = t;
+ tac_redef = [];
+ tac_deprecation = deprecation;
+ } in
mactab := KNmap.add kn entry !mactab
let replace kn path t =
@@ -139,34 +148,38 @@ let replace kn path t =
let entry _ e = { e with tac_body = t; tac_redef = path :: e.tac_redef } in
mactab := KNmap.modify kn entry !mactab
-let load_md i ((sp, kn), (local, id, b, t)) = match id with
+let tac_deprecation kn =
+ try (KNmap.find kn !mactab).tac_deprecation with Not_found -> None
+
+let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
| None ->
let () = if not local then push_tactic (Until i) sp kn in
- add kn b t
+ add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
-let open_md i ((sp, kn), (local, id, b, t)) = match id with
+let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with
| None ->
let () = if not local then push_tactic (Exactly i) sp kn in
- add kn b t
+ add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
-let cache_md ((sp, kn), (local, id ,b, t)) = match id with
+let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with
| None ->
let () = push_tactic (Until 1) sp kn in
- add kn b t
+ add ~deprecation kn b t
| Some kn0 -> replace kn0 kn t
let subst_kind subst id = match id with
| None -> None
| Some kn -> Some (Mod_subst.subst_kn subst kn)
-let subst_md (subst, (local, id, b, t)) =
- (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t)
+let subst_md (subst, (local, id, b, t, deprecation)) =
+ (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t, deprecation)
-let classify_md (local, _, _, _ as o) = Substitute o
+let classify_md (local, _, _, _, _ as o) = Substitute o
-let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
+let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
+ Vernacinterp.deprecation option -> obj =
declare_object {(default_object "TAC-DEFINITION") with
cache_function = cache_md;
load_function = load_md;
@@ -174,8 +187,8 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj =
subst_function = subst_md;
classify_function = classify_md}
-let register_ltac for_ml local id tac =
- ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac)))
+let register_ltac for_ml local ?deprecation id tac =
+ ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac, deprecation)))
-let redefine_ltac local kn tac =
- Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac))
+let redefine_ltac local ?deprecation kn tac =
+ Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac, deprecation))
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index 3af2f2a46..7143f5185 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,6 +12,7 @@ open Names
open Libnames
open Tacexpr
open Geninterp
+open Vernacinterp
(** This module centralizes the various ways of registering tactics. *)
@@ -29,7 +30,11 @@ val shortest_qualid_of_tactic : ltac_constant -> qualid
type alias = KerName.t
(** Type of tactic alias, used in the [TacAlias] node. *)
-type alias_tactic = Id.t list * glob_tactic_expr
+type alias_tactic =
+ { alias_args: Id.t list;
+ alias_body: glob_tactic_expr;
+ alias_deprecation: Vernacinterp.deprecation option;
+ }
(** Contents of a tactic notation *)
val register_alias : alias -> alias_tactic -> unit
@@ -43,7 +48,8 @@ val check_alias : alias -> bool
(** {5 Coq tactic definitions} *)
-val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
+val register_ltac : bool -> bool -> ?deprecation:deprecation -> Id.t ->
+ glob_tactic_expr -> unit
(** Register a new Ltac with the given name and body.
The first boolean indicates whether this is done from ML side, rather than
@@ -51,7 +57,8 @@ val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit
definition. It also puts the Ltac name in the nametab, so that it can be
used unqualified. *)
-val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit
+val redefine_ltac : bool -> ?deprecation:deprecation -> KerName.t ->
+ glob_tactic_expr -> unit
(** Replace a Ltac with the given name and body. If the boolean flag is set
to true, then this is a local redefinition. *)
@@ -61,6 +68,9 @@ val interp_ltac : KerName.t -> glob_tactic_expr
val is_ltac_for_ml_tactic : KerName.t -> bool
(** Whether the tactic is defined from ML-side *)
+val tac_deprecation : KerName.t -> deprecation option
+(** The tactic deprecation notice, if any *)
+
type ltac_entry = {
tac_for_ml : bool;
(** Whether the tactic is defined from ML-side *)
@@ -68,6 +78,8 @@ type ltac_entry = {
(** The current body of the tactic *)
tac_redef : ModPath.t list;
(** List of modules redefining the tactic in reverse chronological order *)
+ tac_deprecation : deprecation option;
+ (** Deprecation notice to be printed when the tactic is used *)
}
val ltac_entries : unit -> ltac_entry KNmap.t
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 06d2711ad..59b748e25 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -398,5 +398,5 @@ type ltac_call_kind =
type ltac_trace = ltac_call_kind Loc.located list
type tacdef_body =
- | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
- | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
+ | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+ | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 71e1edfd7..3a0badb28 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -398,5 +398,5 @@ type ltac_call_kind =
type ltac_trace = ltac_call_kind Loc.located list
type tacdef_body =
- | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
- | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
+ | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *)
+ | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 481fc30df..144480062 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -117,9 +117,26 @@ let intern_constr_reference strict ist qid =
(* Internalize an isolated reference in position of tactic *)
+let warn_deprecated_tactic =
+ CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated"
+ (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++
+ strbrk " is deprecated" ++
+ pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
+ str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+
+let warn_deprecated_alias =
+ CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated"
+ (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++
+ strbrk " is deprecated since" ++
+ pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
+ str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+
let intern_isolated_global_tactic_reference qid =
let loc = qid.CAst.loc in
- TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[]))
+ let kn = Tacenv.locate_tactic qid in
+ Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
+ Tacenv.tac_deprecation kn;
+ TacCall (Loc.tag ?loc (ArgArg (loc,kn),[]))
let intern_isolated_tactic_reference strict ist qid =
(* An ltac reference *)
@@ -137,7 +154,11 @@ let intern_isolated_tactic_reference strict ist qid =
(* Internalize an applied tactic reference *)
let intern_applied_global_tactic_reference qid =
- ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid)
+ let loc = qid.CAst.loc in
+ let kn = Tacenv.locate_tactic qid in
+ Option.iter (fun depr -> warn_deprecated_tactic ?loc (qid,depr)) @@
+ Tacenv.tac_deprecation kn;
+ ArgArg (loc,kn)
let intern_applied_tactic_reference ist qid =
(* An ltac reference *)
@@ -643,6 +664,8 @@ and intern_tactic_seq onlytac ist = function
(* For extensions *)
| TacAlias (loc,(s,l)) ->
+ let alias = Tacenv.interp_alias s in
+ Option.iter (fun o -> warn_deprecated_alias ?loc (s,o)) @@ alias.Tacenv.alias_deprecation;
let l = List.map (intern_tacarg !strict_check false ist) l in
ist.ltacvars, TacAlias (Loc.tag ?loc (s,l))
| TacML (loc,(opn,l)) ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6d94e3f86..a0446bd6a 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1115,17 +1115,17 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias (loc,(s,l)) ->
- let (ids, body) = Tacenv.interp_alias s in
+ let alias = Tacenv.interp_alias s in
let (>>=) = Ftactic.bind in
let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
let tac l =
let addvar x v accu = Id.Map.add x v accu in
- let lfun = List.fold_right2 addvar ids l ist.lfun in
+ let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
let ist = {
lfun = lfun;
extra = TacStore.set ist.extra f_trace trace; } in
- val_interp ist body >>= fun v ->
+ val_interp ist alias.Tacenv.alias_body >>= fun v ->
Ftactic.lift (tactic_of_value ist v)
in
let tac =
@@ -1137,7 +1137,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
some more elaborate solution will have to be used. *)
in
let tac =
- let len1 = List.length ids in
+ let len1 = List.length alias.Tacenv.alias_args in
let len2 = List.length l in
if len1 = len2 then tac
else Tacticals.New.tclZEROMSG (str "Arguments length mismatch: \
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 17:32:47 +0000