From 1bc80b5cf7792e13b9d793de2c8da5192c75920c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 6 Feb 2019 11:57:20 +0100
Subject: 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.
---
 test-suite/success/goal_selector.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'test-suite')

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