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.
---
 user-contrib/Ltac2/tac2entries.ml | 21 ++++-----------------
 1 file changed, 4 insertions(+), 17 deletions(-)

(limited to 'user-contrib')

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