diff options
| author | Gaëtan Gilbert | 2019-02-06 11:57:20 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-08 19:28:53 +0200 |
| commit | 1bc80b5cf7792e13b9d793de2c8da5192c75920c (patch) | |
| tree | ef8cf69a811a0d66a9157bbb9967761c1fb4ca8d /test-suite | |
| parent | 65f75de6929530252a3235af54a0da56980fa02d (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/goal_selector.v | 8 |
1 files changed, 5 insertions, 3 deletions
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. |