From cbe88ec043df8dff118e437f00c0299a464c8e8a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 22 Mar 2021 12:42:02 +0100
Subject: Factorize goal selector handling

As a bonus ltac2 can produce bullet suggestions.
---
 tactics/tacticals.ml  | 11 ++---------
 tactics/tacticals.mli |  4 +++-
 2 files changed, 5 insertions(+), 10 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3