Factorize goal selector handling

As a bonus ltac2 can produce bullet suggestions.

1 files changed, 4 insertions, 17 deletions

diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index faa1e74728..5ddf56402f 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -811,24 +811,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