aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/evar_tactics.ml4
-rw-r--r--plugins/ltac/extratactics.ml42
-rw-r--r--plugins/ltac/g_ltac.ml43
-rw-r--r--plugins/ltac/pptactic.ml1
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/rewrite.ml7
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacexpr.ml5
-rw-r--r--plugins/ltac/tacexpr.mli5
-rw-r--r--plugins/ltac/tacinterp.ml9
-rw-r--r--plugins/ltac/tactic_matching.ml2
11 files changed, 21 insertions, 21 deletions
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 9382f567b4..fb6be430fc 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -85,9 +85,7 @@ let let_evar name typ =
Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
- let sigma = ref sigma in
- let _ = Typing.e_sort_of env sigma typ in
- let sigma = !sigma in
+ let sigma, _ = Typing.sort_of env sigma typ in
let id = match name with
| Name.Anonymous ->
let id = Namegen.id_of_name_using_hdchar env sigma typ name in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index a5f8060aee..797dfbe23f 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -315,7 +315,7 @@ let project_hint ~poly pri l2r r =
let ctx = Evd.const_univ_entry ~poly sigma in
let c = EConstr.to_constr sigma c in
let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
- let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
+ let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
(info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
let add_hints_iff ~atts l2r lc n bl =
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 0c42a8bb28..4857beffa8 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -325,6 +325,7 @@ GEXTEND Gram
;
toplevel_selector:
[ [ sel = selector_body; ":" -> sel
+ | "!"; ":" -> SelectAlreadyFocused
| IDENT "all"; ":" -> SelectAll ] ]
;
tactic_mode:
@@ -415,7 +416,7 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false
VERNAC tactic_mode EXTEND VernacSolve
| [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
[ classify_as_proofstep ] -> [
- let g = Option.default (Proof_bullet.get_default_goal_selector ()) g in
+ let g = Option.default (Goal_select.get_default_goal_selector ()) g in
vernac_solve g n t def
]
| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 11bb7a2341..bd02d85d59 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -515,6 +515,7 @@ let string_of_genarg_arg (ArgumentType arg) =
else int i ++ str "-" ++ int j
let pr_goal_selector toplevel = function
+ | SelectAlreadyFocused -> str "!:"
| SelectNth i -> int i ++ str ":"
| SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":"
| SelectId id -> str "[" ++ Id.print id ++ str "]:"
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index aea00c240b..799a52cc8b 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -84,7 +84,7 @@ type pp_tactic = {
pptac_prods : grammar_terminals;
}
-val pr_goal_selector : toplevel:bool -> Vernacexpr.goal_selector -> Pp.t
+val pr_goal_selector : toplevel:bool -> Goal_select.t -> Pp.t
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9eb55aa5e5..1b86583da1 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -104,9 +104,8 @@ let extends_undefined evars evars' =
let app_poly_check env evars f args =
let (evars, cstrs), fc = f evars in
- let evdref = ref evars in
- let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in
- (!evdref, cstrs), t
+ let evars, t = Typing.solve_evars env evars (mkApp (fc, args)) in
+ (evars, cstrs), t
let app_poly_nocheck env evars f args =
let evars, fc = f evars in
@@ -1469,8 +1468,8 @@ exception RewriteFailure of Pp.t
type result = (evar_map * constr option * types) option option
let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result =
+ let sigma, sort = Typing.sort_of env sigma concl in
let evdref = ref sigma in
- let sort = Typing.e_sort_of env evdref concl in
let evars = (!evdref, Evar.Set.empty) in
let evars, cstr =
let prop, (evars, arrow) =
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 1fa5e3c076..5185217cda 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -80,7 +80,7 @@ val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t
val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list
-val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> Globnames.global_reference
+val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> GlobRef.t
val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 3baa475aba..17f5e5d41a 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -35,7 +35,8 @@ type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-type goal_selector = Vernacexpr.goal_selector =
+type goal_selector = Goal_select.t =
+ | SelectAlreadyFocused
| SelectNth of int
| SelectList of (int * int) list
| SelectId of Id.t
@@ -269,7 +270,7 @@ and 'a gen_tactic_expr =
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg located
- | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr
+ | TacSelect of Goal_select.t * 'a gen_tactic_expr
(* For ML extensions *)
| TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
(* For syntax extensions *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 3baa475aba..17f5e5d41a 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -35,7 +35,8 @@ type advanced_flag = bool (* true = advanced false = basic *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
-type goal_selector = Vernacexpr.goal_selector =
+type goal_selector = Goal_select.t =
+ | SelectAlreadyFocused
| SelectNth of int
| SelectList of (int * int) list
| SelectId of Id.t
@@ -269,7 +270,7 @@ and 'a gen_tactic_expr =
('p,'a gen_tactic_expr) match_rule list
| TacFun of 'a gen_tactic_fun_ast
| TacArg of 'a gen_tactic_arg located
- | TacSelect of Vernacexpr.goal_selector * 'a gen_tactic_expr
+ | TacSelect of Goal_select.t * 'a gen_tactic_expr
(* For ML extensions *)
| TacML of (ml_tactic_entry * 'a gen_tactic_arg list) Loc.located
(* For syntax extensions *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6a4bf577b1..a93cf5ae7c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -691,11 +691,9 @@ let interp_may_eval f ist env sigma = function
let (sigma,ic) = f ist env sigma c in
let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
let ctxt = EConstr.Unsafe.to_constr ctxt in
- let evdref = ref sigma in
- let ic = EConstr.Unsafe.to_constr ic in
+ let ic = EConstr.Unsafe.to_constr ic in
let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
- let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
- !evdref , c
+ Typing.solve_evars env sigma (EConstr.of_constr c)
with
| Not_found ->
user_err ?loc ~hdr:"interp_may_eval"
@@ -2010,7 +2008,8 @@ let interp_redexp env sigma r =
let _ =
let eval lfun env sigma ty tac =
- let ist = { lfun = lfun; extra = TacStore.empty; } in
+ let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
+ let ist = { lfun = lfun; extra; } in
let tac = interp_tactic ist tac in
let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
(EConstr.of_constr c, sigma)
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index b6462c8106..c949589e22 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -46,7 +46,7 @@ let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map ->
(** Adds a binding to a {!Id.Map.t} if the identifier is [Some id] *)
let id_map_try_add id x m =
match id with
- | Some id -> Id.Map.add id x m
+ | Some id -> Id.Map.add id (Lazy.force x) m
| None -> m
(** Adds a binding to a {!Id.Map.t} if the name is [Name id] *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 07:44:03 +0000