aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--proofs/goal_select.ml19
-rw-r--r--proofs/goal_select.mli2
-rw-r--r--proofs/proof.ml20
-rw-r--r--proofs/proofs.mllib2
-rw-r--r--tactics/tacticals.ml11
-rw-r--r--tactics/tacticals.mli4
-rw-r--r--user-contrib/Ltac2/tac2entries.ml21
8 files changed, 33 insertions, 48 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 54d7c310aa..da95869abb 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1180,7 +1180,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
| TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
| TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v)
- | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
+ | TacSelect (sel, tac) -> Goal_select.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
let alias = Tacenv.interp_alias s in
diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
index e847535aaf..68646c93c9 100644
--- a/proofs/goal_select.ml
+++ b/proofs/goal_select.ml
@@ -57,3 +57,22 @@ let get_default_goal_selector =
~value:(SelectNth 1)
parse_goal_selector
(fun v -> Pp.string_of_ppcmds @@ pr_goal_selector v)
+
+(* Select a subset of the goals *)
+let tclSELECT ?nosuchgoal g tac = match g with
+ | SelectNth i -> Proofview.tclFOCUS ?nosuchgoal i i tac
+ | SelectList l -> Proofview.tclFOCUSLIST ?nosuchgoal l tac
+ | SelectId id -> Proofview.tclFOCUSID ?nosuchgoal id tac
+ | SelectAll -> tac
+ | SelectAlreadyFocused ->
+ let open Proofview.Notations in
+ Proofview.numgoals >>= fun n ->
+ if n == 1 then tac
+ else
+ let e = CErrors.UserError
+ (None,
+ Pp.(str "Expected a single focused goal but " ++
+ int n ++ str " goals are focused."))
+ in
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info e
diff --git a/proofs/goal_select.mli b/proofs/goal_select.mli
index 977392baa6..c6726300f0 100644
--- a/proofs/goal_select.mli
+++ b/proofs/goal_select.mli
@@ -24,3 +24,5 @@ type t =
val pr_goal_selector : t -> Pp.t
val get_default_goal_selector : unit -> t
+
+val tclSELECT : ?nosuchgoal:'a Proofview.tactic -> t -> 'a Proofview.tactic -> 'a Proofview.tactic
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 50a0e63700..e535536472 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -538,25 +538,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
let info = Exninfo.reify () in
Proofview.tclZERO ~info (SuggestNoSuchGoals (1,pr))
in
- let tac = let open Goal_select in match gi with
- | SelectAlreadyFocused ->
- let open Proofview.Notations in
- Proofview.numgoals >>= fun n ->
- if n == 1 then tac
- else
- let e = CErrors.UserError
- (None,
- Pp.(str "Expected a single focused goal but " ++
- int n ++ str " goals are focused."))
- in
- let info = Exninfo.reify () in
- Proofview.tclZERO ~info e
-
- | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
- | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
- | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
- | SelectAll -> tac
- in
+ let tac = Goal_select.tclSELECT ~nosuchgoal gi tac in
let tac =
if use_unification_heuristics () then
Proofview.tclTHEN tac Refine.solve_constraints
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 5f19c1bb09..43cde83e58 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -2,9 +2,9 @@ Miscprint
Goal
Evar_refiner
Refine
+Goal_select
Proof
Logic
-Goal_select
Proof_bullet
Tacmach
Clenv
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 68afd9a128..2d69047d1e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -683,15 +683,6 @@ module New = struct
let tclPROGRESS t =
Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t)
- (* Select a subset of the goals *)
- let tclSELECT = let open Goal_select in function
- | SelectNth i -> Proofview.tclFOCUS i i
- | SelectList l -> Proofview.tclFOCUSLIST l
- | SelectId id -> Proofview.tclFOCUSID id
- | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
- | SelectAlreadyFocused ->
- anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here")
-
(* Check that holes in arguments have been resolved *)
let check_evars env sigma extsigma origsigma =
@@ -905,4 +896,6 @@ module New = struct
let (sigma, t) = Typing.type_of ?refresh env sigma c in
Proofview.Unsafe.tclEVARS sigma <*> tac sigma t)
+ let tclSELECT = Goal_select.tclSELECT
+
end
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 19d08dcc36..c09d268c40 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -206,7 +206,6 @@ module New : sig
val tclCOMPLETE : 'a tactic -> 'a tactic
val tclSOLVE : unit tactic list -> unit tactic
val tclPROGRESS : unit tactic -> unit tactic
- val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic
val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic
val tclMAPDELAYEDWITHHOLES : bool -> 'a delayed_open list -> ('a -> unit tactic) -> unit tactic
@@ -250,4 +249,7 @@ module New : sig
val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic
val tclTYPEOFTHEN : ?refresh:bool -> constr -> (evar_map -> types -> unit Proofview.tactic) -> unit Proofview.tactic
+
+ val tclSELECT : ?nosuchgoal:'a tactic -> Goal_select.t -> 'a tactic -> 'a tactic
+ [@@ocaml.deprecated "Use [Goal_select.tclSELECT]"]
end
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 0aa05934bf..d2e74609a2 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -841,24 +841,11 @@ let perform_eval ~pstate e =
Goal_select.get_default_goal_selector (),
Declare.Proof.get pstate
in
- let v = match selector with
- | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v
- | Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v
- | Goal_select.SelectId id -> Proofview.tclFOCUSID id v
- | Goal_select.SelectAll -> v
- | Goal_select.SelectAlreadyFocused ->
- let open Proofview.Notations in
- Proofview.numgoals >>= fun n ->
- if Int.equal n 1 then v
- else
- let e = CErrors.UserError
- (None,
- Pp.(str "Expected a single focused goal but " ++
- int n ++ str " goals are focused."))
- in
- let info = Exninfo.reify () in
- Proofview.tclZERO ~info e
+ let nosuchgoal =
+ let info = Exninfo.reify () in
+ Proofview.tclZERO ~info (Proof.SuggestNoSuchGoals (1,proof))
in
+ let v = Goal_select.tclSELECT ~nosuchgoal selector v in
let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in
let { Proof.sigma } = Proof.data proof in
let name = int_name () in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:04:02 +0000