aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml2
-rw-r--r--plugins/ltac/extratactics.ml44
-rw-r--r--plugins/ltac/g_ltac.ml411
-rw-r--r--plugins/ltac/pptactic.ml26
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/rewrite.ml6
-rw-r--r--plugins/ltac/rewrite.mli2
-rw-r--r--plugins/ltac/tacentries.ml1
-rw-r--r--plugins/ltac/tacinterp.ml38
-rw-r--r--plugins/ltac/tacinterp.mli4
10 files changed, 48 insertions, 48 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 4cab6ef336..d9150a7bbd 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -88,7 +88,7 @@ let let_evar name typ =
let id = match name with
| Name.Anonymous ->
let id = Namegen.id_of_name_using_hdchar env sigma typ name in
- Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
+ Namegen.next_ident_away_in_goal id (Termops.vars_of_env env)
| Name.Name id -> id
in
let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index b4c6f9c90e..a7aebf9e15 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -665,7 +665,7 @@ let hResolve id c occ t =
let sigma = Proofview.Goal.sigma gl in
let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
let concl = Proofview.Goal.concl gl in
- let env_ids = Termops.ids_of_context env in
+ let env_ids = Termops.vars_of_env env in
let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in
let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in
let rec resolve_hole t_hole =
@@ -764,7 +764,7 @@ let case_eq_intros_rewrite x =
mkCaseEq x;
Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
- let hyps = Tacmach.New.pf_ids_of_hyps gl in
+ let hyps = Tacmach.New.pf_ids_set_of_hyps gl in
let n' = nb_prod (Tacmach.New.project gl) concl in
let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in
Tacticals.New.tclTHENLIST [
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 2ea0f60ebc..86c983bdd9 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -388,16 +388,7 @@ let vernac_solve n info tcom b =
p,status) in
if not status then Feedback.feedback Feedback.AddedAxiom
-let pr_range_selector (i, j) =
- if Int.equal i j then int i
- else int i ++ str "-" ++ int j
-
-let pr_ltac_selector = function
-| SelectNth i -> int i ++ str ":"
-| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
- str "]" ++ str ":"
-| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
-| SelectAll -> str "all" ++ str ":"
+let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
| [ toplevel_selector(s) ] -> [ s ]
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index f4e3ba633f..d8bd166208 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -477,12 +477,14 @@ type 'a extra_genarg_printer =
if Int.equal i j then int i
else int i ++ str "-" ++ int j
- let pr_goal_selector = function
- | SelectNth i -> int i ++ str ":"
- | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
- str "]" ++ str ":"
- | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
- | SelectAll -> str "all" ++ str ":"
+let pr_goal_selector toplevel = function
+ | SelectNth i -> int i ++ str ":"
+ | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":"
+ | SelectId id -> str "[" ++ Id.print id ++ str "]:"
+ | SelectAll -> assert toplevel; str "all:"
+
+let pr_goal_selector ~toplevel s =
+ (if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s
let pr_lazy = function
| General -> keyword "multi"
@@ -662,14 +664,14 @@ type 'a extra_genarg_printer =
let names =
List.fold_left
(fun ln (nal,_) -> List.fold_left
- (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+ (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln)
ln nal)
- [] bll in
+ Id.Set.empty bll in
let idarg,bll = set_nth_name names n bll in
- let annot = match names with
- | [_] ->
+ let annot =
+ if Int.equal (Id.Set.cardinal names) 1 then
mt ()
- | _ ->
+ else
spc() ++ str"{"
++ keyword "struct" ++ spc ()
++ pr_id idarg ++ str"}"
@@ -988,7 +990,7 @@ type 'a extra_genarg_printer =
keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
| TacComplete t ->
pr_tac (lcomplete,E) t, lcomplete
- | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom
+ | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom
| TacId l ->
keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
| TacAtom (loc,t) ->
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 1f6ebaf448..c79d5b389f 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -53,6 +53,8 @@ type pp_tactic = {
pptac_prods : grammar_terminals;
}
+val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t
+
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
val pr_with_occurrences :
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 75b665aad9..fd791a9101 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -664,7 +664,7 @@ type rewrite_result =
type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *)
env : Environ.env ;
- unfresh : Id.t list ; (* Unfresh names *)
+ unfresh : Id.Set.t; (* Unfresh names *)
term1 : constr ;
ty1 : types ; (* first term and its type (convertible to rew_from) *)
cstr : (bool (* prop *) * constr option) ;
@@ -1614,7 +1614,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
in
try
let res =
- cl_rewrite_clause_aux ?abs strat env [] sigma ty clause
+ cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause
in
let sigma = match origsigma with None -> sigma | Some sigma -> sigma in
treat sigma res <*>
@@ -1884,7 +1884,7 @@ let declare_projection n instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let typ = it_mkProd_or_LetIn typ ctx in
- let pl, ctx = Evd.universe_context sigma in
+ let pl, ctx = Evd.universe_context ~names:[] ~extensible:true sigma in
let typ = EConstr.to_constr sigma typ in
let term = EConstr.to_constr sigma term in
let cst =
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 23767c12f5..63e891b455 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -110,7 +110,7 @@ val setoid_transitivity : constr option -> unit Proofview.tactic
val apply_strategy :
strategy ->
Environ.env ->
- Names.Id.t list ->
+ Names.Id.Set.t ->
constr ->
bool * constr ->
evars -> rewrite_result
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index cf676f598f..a8d518fbd8 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -216,7 +216,6 @@ let interp_prod_item = function
assert (String.equal s "tactic");
begin match Tacarg.wit_tactic with
| ExtraArg tag -> ArgT.Any tag
- | _ -> assert false
end
in
let symbol = interp_entry_name interp symbol in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 8fa95ffb02..20f117ff4f 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -139,7 +139,7 @@ let name_vfun appl vle =
module TacStore = Geninterp.TacStore
-let f_avoid_ids : Id.t list TacStore.field = TacStore.field ()
+let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field ()
(* ids inherited from the call context (needed to get fresh ids) *)
let f_debug : debug_info TacStore.field = TacStore.field ()
let f_trace : ltac_trace TacStore.field = TacStore.field ()
@@ -501,29 +501,29 @@ let extract_ltac_constr_values ist env =
could barely be defined as a feature... *)
(* Extract the identifier list from lfun: join all branches (what to do else?)*)
-let rec intropattern_ids (loc,pat) = match pat with
- | IntroNaming (IntroIdentifier id) -> [id]
+let rec intropattern_ids accu (loc,pat) = match pat with
+ | IntroNaming (IntroIdentifier id) -> Id.Set.add id accu
| IntroAction (IntroOrAndPattern (IntroAndPattern l)) ->
- List.flatten (List.map intropattern_ids l)
+ List.fold_left intropattern_ids accu l
| IntroAction (IntroOrAndPattern (IntroOrPattern ll)) ->
- List.flatten (List.map intropattern_ids (List.flatten ll))
+ List.fold_left intropattern_ids accu (List.flatten ll)
| IntroAction (IntroInjection l) ->
- List.flatten (List.map intropattern_ids l)
- | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat
+ List.fold_left intropattern_ids accu l
+ | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids accu pat
| IntroNaming (IntroAnonymous | IntroFresh _)
| IntroAction (IntroWildcard | IntroRewrite _)
- | IntroForthcoming _ -> []
+ | IntroForthcoming _ -> accu
-let extract_ids ids lfun =
+let extract_ids ids lfun accu =
let fold id v accu =
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
let (_, ipat) = out_gen (topwit wit_intro_pattern) v in
if Id.List.mem id ids then accu
- else accu @ intropattern_ids (Loc.tag ipat)
+ else intropattern_ids accu (Loc.tag ipat)
else accu
in
- Id.Map.fold fold lfun []
+ Id.Map.fold fold lfun accu
let default_fresh_id = Id.of_string "H"
@@ -534,10 +534,10 @@ let interp_fresh_id ist env sigma l =
with Not_found -> id in
let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
let avoid = match TacStore.get ist.extra f_avoid_ids with
- | None -> []
+ | None -> Id.Set.empty
| Some l -> l
in
- let avoid = (extract_ids ids ist.lfun) @ avoid in
+ let avoid = extract_ids ids ist.lfun avoid in
let id =
if List.is_empty l then default_fresh_id
else
@@ -1303,7 +1303,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v
end
| ArgArg (loc,r) ->
- let ids = extract_ids [] ist.lfun in
+ let ids = extract_ids [] ist.lfun Id.Set.empty in
let loc_info = (Option.default loc loc',LtacNameCall r) in
let extra = TacStore.set ist.extra f_avoid_ids ids in
push_trace loc_info ist >>= fun trace ->
@@ -1394,7 +1394,13 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
else
Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body)))
- | _ -> fail
+ | (VFun(appl,trace,olfun,[],body)) ->
+ let extra_args = List.length largs in
+ Tacticals.New.tclZEROMSG (str "Illegal tactic application: got " ++
+ str (string_of_int extra_args) ++
+ str " extra " ++ str (String.plural extra_args "argument") ++
+ str ".")
+ | VRec(_,_) -> fail
else fail
(* Gives the tactic corresponding to the tactic value *)
@@ -1956,7 +1962,7 @@ let interp_tac_gen lfun avoid_ids debug t =
(intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
end
-let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t
+let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t
(* Used to hide interpretation for pretty-print, now just launch tactics *)
(* [global] means that [t] should be internalized outside of goals. *)
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index c1ab2b4c49..d0a0a81d4c 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -40,7 +40,7 @@ type interp_sign = Geninterp.interp_sign = {
lfun : value Id.Map.t;
extra : TacStore.t }
-val f_avoid_ids : Id.t list TacStore.field
+val f_avoid_ids : Id.Set.t TacStore.field
val f_debug : debug_info TacStore.field
val extract_ltac_constr_values : interp_sign -> Environ.env ->
@@ -113,7 +113,7 @@ val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic
(** Globalization + interpretation *)
-val interp_tac_gen : value Id.Map.t -> Id.t list ->
+val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
debug_info -> raw_tactic_expr -> unit Proofview.tactic
val interp : raw_tactic_expr -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 16:59:10 +0000