aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/g_auto.ml41
-rw-r--r--plugins/ltac/g_class.ml41
-rw-r--r--plugins/ltac/g_eqdecide.ml41
-rw-r--r--plugins/ltac/g_ltac.ml49
-rw-r--r--plugins/ltac/g_tactic.ml45
-rw-r--r--plugins/ltac/pptactic.ml4
-rw-r--r--plugins/ltac/tacentries.ml17
-rw-r--r--plugins/ltac/tacentries.mli2
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml10
-rw-r--r--plugins/ltac/tacinterp.ml25
-rw-r--r--plugins/ltac/tacinterp.mli2
-rw-r--r--plugins/ltac/tacsubst.ml4
-rw-r--r--plugins/ltac/tauto.ml2
14 files changed, 46 insertions, 39 deletions
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 4ec42c676f..fcc2b86a91 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -16,6 +16,7 @@ open Pcoq.Constr
open Pltac
open Hints
open Tacexpr
+open Names
DECLARE PLUGIN "g_auto"
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index a28132a4b0..ca9537c824 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -13,6 +13,7 @@ open Class_tactics
open Pltac
open Stdarg
open Tacarg
+open Names
DECLARE PLUGIN "g_class"
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 905653281c..679aa11272 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -15,6 +15,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Eqdecide
+open Names
DECLARE PLUGIN "g_eqdecide"
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 54229bb2ae..aab5687465 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -17,6 +17,7 @@ open Misctypes
open Genarg
open Genredexpr
open Tok (* necessary for camlp4 *)
+open Names
open Pcoq
open Pcoq.Constr
@@ -226,8 +227,8 @@ GEXTEND Gram
| "multimatch" -> General ] ]
;
input_fun:
- [ [ "_" -> None
- | l = ident -> Some l ] ]
+ [ [ "_" -> Anonymous
+ | l = ident -> Name l ] ]
;
let_clause:
[ [ id = identref; ":="; te = tactic_expr ->
@@ -499,8 +500,8 @@ let pr_tacdef_body tacdef_body =
| Tacexpr.TacFun (idl,b) -> idl,b
| _ -> [], body in
id ++
- prlist (function None -> str " _"
- | Some id -> spc () ++ Nameops.pr_id id) idl
+ prlist (function Anonymous -> str " _"
+ | Name id -> spc () ++ Nameops.pr_id id) idl
++ (if redef then str" ::=" else str" :=") ++ brk(1,1)
++ Pptactic.pr_raw_tactic body
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 685c07c9a8..fa01baab75 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -325,8 +325,9 @@ GEXTEND Gram
l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
let loc0,pat = pat in
let f c pat =
- let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in
- IntroAction (IntroApplyOn (c,(loc,pat))) in
+ let loc1 = Constrexpr_ops.constr_loc c in
+ let loc = Loc.merge loc0 loc1 in
+ IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in
!@loc, List.fold_right f l pat ] ]
;
simple_intropattern_closed:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index fccee6e40a..6f4ef37b44 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -574,9 +574,7 @@ module Make
str "=>" ++ brk (1,4) ++ pr t))
| All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
- let pr_funvar = function
- | None -> spc () ++ str "_"
- | Some id -> spc () ++ pr_id id
+ let pr_funvar n = spc () ++ pr_name n
let pr_let_clause k pr (id,(bl,t)) =
hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 2e2b55be74..cd8c9e471e 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -302,9 +302,9 @@ let cons_production_parameter = function
| TacTerm _ -> None
| TacNonTerm (_, _, id) -> Some id
-let add_glob_tactic_notation local n prods forml ids tac =
+let add_glob_tactic_notation local ~level prods forml ids tac =
let parule = {
- tacgram_level = n;
+ tacgram_level = level;
tacgram_prods = prods;
} in
let tacobj = {
@@ -360,7 +360,7 @@ let extend_atomic_tactic name entries =
in
List.iteri add_atomic entries
-let add_ml_tactic_notation name prods =
+let add_ml_tactic_notation name ~level prods =
let len = List.length prods in
let iter i prods =
let open Tacexpr in
@@ -372,10 +372,12 @@ let add_ml_tactic_notation name prods =
let entry = { mltac_name = name; mltac_index = len - i - 1 } in
let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in
let tac = TacML (Loc.ghost, entry, List.map map ids) in
- add_glob_tactic_notation false 0 prods true ids tac
+ add_glob_tactic_notation false ~level prods true ids tac
in
List.iteri iter (List.rev prods);
- extend_atomic_tactic name prods
+ (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
+ tactic_expr level 0) *)
+ if Int.equal level 0 then extend_atomic_tactic name prods
(**********************************************************************)
(** Ltac quotations *)
@@ -504,10 +506,7 @@ let print_ltacs () =
| Tacexpr.TacFun (l, t) -> (l, t)
| _ -> ([], body)
in
- let pr_ltac_fun_arg = function
- | None -> spc () ++ str "_"
- | Some id -> spc () ++ pr_id id
- in
+ let pr_ltac_fun_arg n = spc () ++ pr_name n in
hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l)
in
Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 969c118fb5..0695044736 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -45,7 +45,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 ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int ->
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. *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9c25a16457..e23992a807 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -282,7 +282,7 @@ constraint 'a = <
>
and 'a gen_tactic_fun_ast =
- Id.t option list * 'a gen_tactic_expr
+ Name.t list * 'a gen_tactic_expr
constraint 'a = <
term:'t;
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 4b5d87fc3c..3f83f104e9 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -248,8 +248,8 @@ and intern_intro_pattern_action lf ist = function
| IntroInjection l ->
IntroInjection (List.map (intern_intro_pattern lf ist) l)
| IntroWildcard | IntroRewrite _ as x -> x
- | IntroApplyOn (c,pat) ->
- IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat)
+ | IntroApplyOn ((loc,c),pat) ->
+ IntroApplyOn ((loc,intern_constr ist c), intern_intro_pattern lf ist pat)
and intern_or_and_intro_pattern lf ist = function
| IntroAndPattern l ->
@@ -646,7 +646,7 @@ and intern_tactic_or_tacarg ist = intern_tactic false ist
and intern_pure_tactic ist = intern_tactic true ist
and intern_tactic_fun ist (var,body) =
- let lfun = List.fold_left opt_cons ist.ltacvars var in
+ let lfun = List.fold_left name_cons ist.ltacvars var in
(var,intern_tactic_or_tacarg { ist with ltacvars = lfun } body)
and intern_tacarg strict onlytac ist = function
@@ -722,9 +722,7 @@ let split_ltac_fun = function
| TacFun (l,t) -> (l,t)
| t -> ([],t)
-let pr_ltac_fun_arg = function
- | None -> spc () ++ str "_"
- | Some id -> spc () ++ pr_id id
+let pr_ltac_fun_arg n = spc () ++ pr_name n
let print_ltac id =
try
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fda9142eda..155cb31d85 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -120,7 +120,7 @@ let combine_appl appl1 appl2 =
(* Values for interpretation *)
type tacvalue =
| VFun of appl*ltac_trace * value Id.Map.t *
- Id.t option list * glob_tactic_expr
+ Name.t list * glob_tactic_expr
| VRec of value Id.Map.t ref * glob_tactic_expr
let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
@@ -520,7 +520,7 @@ let rec intropattern_ids (loc,pat) = match pat with
List.flatten (List.map intropattern_ids (List.flatten ll))
| IntroAction (IntroInjection l) ->
List.flatten (List.map intropattern_ids l)
- | IntroAction (IntroApplyOn (c,pat)) -> intropattern_ids pat
+ | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat
| IntroNaming (IntroAnonymous | IntroFresh _)
| IntroAction (IntroWildcard | IntroRewrite _)
| IntroForthcoming _ -> []
@@ -913,14 +913,14 @@ and interp_intro_pattern_action ist env sigma = function
| IntroInjection l ->
let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
sigma, IntroInjection l
- | IntroApplyOn (c,ipat) ->
+ | IntroApplyOn ((loc,c),ipat) ->
let c = { delayed = fun env sigma ->
let sigma = Sigma.to_evar_map sigma in
let (sigma, c) = interp_open_constr ist env sigma c in
Sigma.Unsafe.of_pair (c, sigma)
} in
let sigma,ipat = interp_intro_pattern ist env sigma ipat in
- sigma, IntroApplyOn (c,ipat)
+ sigma, IntroApplyOn ((loc,c),ipat)
| IntroWildcard | IntroRewrite _ as x -> sigma, x
and interp_or_and_intro_pattern ist env sigma = function
@@ -1087,8 +1087,8 @@ let head_with_value (lvar,lval) =
| ([],[]) -> (lacc,[],[])
| (vr::tvr,ve::tve) ->
(match vr with
- | None -> head_with_value_rec lacc (tvr,tve)
- | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
+ | Anonymous -> head_with_value_rec lacc (tvr,tve)
+ | Name v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
| (vr,[]) -> (lacc,vr,[])
| ([],ve) -> (lacc,[],ve)
in
@@ -1422,7 +1422,14 @@ and tactic_of_value ist vle =
extra = TacStore.set ist.extra f_trace []; } in
let tac = name_if_glob appl (eval_tactic ist t) in
Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
- | (VFun _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
+ | VFun (_, _, _,vars,_) ->
+ let numargs = List.length vars in
+ Tacticals.New.tclZEROMSG
+ (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++
+ Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++
+ Pp.str (String.plural numargs "variable") ++ Pp.str " " ++
+ pr_enum pr_name vars ++ Pp.str ".")
+ | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
else if has_type vle (topwit wit_tactic) then
let tac = out_gen (topwit wit_tactic) vle in
tactic_of_value ist tac
@@ -2120,8 +2127,8 @@ let lift_constr_tac_to_ml_tac vars tac =
let env = Proofview.Goal.env gl in
let sigma = project gl in
let map = function
- | None -> None
- | Some id ->
+ | Anonymous -> None
+ | Name id ->
let c = Id.Map.find id ist.lfun in
try Some (coerce_to_closed_constr env c)
with CannotCoerceTo ty ->
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 6f64981eff..adbd1d32be 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -115,7 +115,7 @@ val error_ltac_variable : Loc.t -> Id.t ->
(** Transforms a constr-expecting tactic into a tactic finding its arguments in
the Ltac environment according to the given names. *)
-val lift_constr_tac_to_ml_tac : Id.t option list ->
+val lift_constr_tac_to_ml_tac : Name.t list ->
(constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic
val default_ist : unit -> Geninterp.interp_sign
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index b09bdda65c..fe3a9f3b2a 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -51,8 +51,8 @@ let rec subst_intro_pattern subst = function
| loc, IntroNaming _ | loc, IntroForthcoming _ as x -> x
and subst_intro_pattern_action subst = function
- | IntroApplyOn (t,pat) ->
- IntroApplyOn (subst_glob_constr subst t,subst_intro_pattern subst pat)
+ | IntroApplyOn ((loc,t),pat) ->
+ IntroApplyOn ((loc,subst_glob_constr subst t),subst_intro_pattern subst pat)
| IntroOrAndPattern l ->
IntroOrAndPattern (subst_intro_or_and_pattern subst l)
| IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l)
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 756958c2f0..fb05fd7d0e 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -259,7 +259,7 @@ let with_flags flags _ ist =
let register_tauto_tactic tac name0 args =
let ids = List.map (fun id -> Id.of_string id) args in
- let ids = List.map (fun id -> Some id) ids in
+ let ids = List.map (fun id -> Name id) ids in
let name = { mltac_plugin = tauto_plugin; mltac_tactic = name0; } in
let entry = { mltac_name = name; mltac_index = 0 } in
let () = Tacenv.register_ml_tactic name [| tac |] in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 07:53:15 +0000