Test goal range in "only" selectors

I don't know what goal_selector.v was supposed to test but CI says
nobody relied on it.

3 files changed, 26 insertions, 28 deletions

diff --git a/doc/changelog/04-tactics/10318-select-only-error.rst b/doc/changelog/04-tactics/10318-select-only-error.rst
new file mode 100644
index 0000000000..03ed15d948
--- /dev/null
+++ b/doc/changelog/04-tactics/10318-select-only-error.rst
@@ -0,0 +1,4 @@
+- The goal selector tactical ``only`` now checks that the goal range
+  it is given is valid instead of ignoring goals out of the focus
+  range. (`#10318 <https://github.com/coq/coq/pull/10318>`_, by Gaëtan
+  Gilbert).
diff --git a/engine/proofview.ml b/engine/proofview.ml
index c00c90e5e9..d4f6fe3aef 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -373,32 +373,24 @@ let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
 let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t =
   let open Proof in
   Comb.get >>= fun comb ->
-    let n = CList.length comb in
-    (* First, remove empty intervals, and bound the intervals to the number
-       of goals. *)
-    let sanitize (i, j) =
-      if i > j then None
-      else if i > n then None
-      else if j < 1 then None
-      else Some ((max i 1), (min j n))
-    in
-    let l = CList.map_filter sanitize l in
+  let n = CList.length comb in
+  let ok (i, j) = 1 <= i && i <= j && j <= n in
+  if not (CList.for_all ok l) then nosuchgoal
+  else
     match l with
-      | [] -> nosuchgoal
-      | (mi, _) :: _ ->
-          (* Get the left-most goal to focus. This goal won't move, and we
-             will then place all the other goals to focus to the right. *)
-          let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in
-          (* [CList.goto] returns a zipper, so that
-             [(rev left) @ sub_right = comb]. *)
-          let left, sub_right = CList.goto (mi-1) comb in
-          let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in
-          let sub, right = CList.partitioni p sub_right in
-          let mj = mi - 1 + CList.length sub in
-            Comb.set (CList.rev_append left (sub @ right)) >>
-            tclFOCUS mi mj t
-
-
+    | [] -> nosuchgoal
+    | (mi, _) :: _ ->
+      (* Get the left-most goal to focus. This goal won't move, and we
+         will then place all the other goals to focus to the right. *)
+      let mi = CList.fold_left (fun m (i, _) -> min m i) mi l in
+      (* [CList.goto] returns a zipper, so that
+         [(rev left) @ sub_right = comb]. *)
+      let left, sub_right = CList.goto (mi-1) comb in
+      let p x _ = CList.exists (fun (i, j) -> i <= x + mi && x + mi <= j) l in
+      let sub, right = CList.partitioni p sub_right in
+      let mj = mi - 1 + CList.length sub in
+      Comb.set (CList.rev_append left (sub @ right)) >>
+      tclFOCUS mi mj t
 
 (** Like {!tclFOCUS} but selects a single goal by name. *)
 let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 0951c5c8d4..ae834e7696 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -13,13 +13,15 @@ Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true.
 Proof.
   do 2 dup.
   - repeat split.
-    2, 4-99, 100-3:idtac.
+    Fail 7:idtac.
+    Fail 2-1:idtac.
+    1,2,4-6:idtac.
     2-5:exact One.
     par:exact Zero.
   - repeat split.
     3-6:swap 1 4.
     1-5:swap 1 5.
-    0-4:exact One.
+    1-4:exact One.
     all:exact Zero.
   - repeat split.
     1, 3:exact Zero.
@@ -34,7 +36,7 @@ Qed.
 
 Goal True -> True.
 Proof.
-  intros y; only 1-2 : repeat idtac.
+  intros y.
   1-1:match goal with y : _ |- _ => let x := y in idtac x end.
   Fail 1-1:let x := y in idtac x.
   1:let x := y in idtac x.