diff options
| author | Pierre-Marie Pédrot | 2019-06-08 22:33:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-08 22:33:14 +0200 |
| commit | a999ff029d7eca67531adfb4c7d6aeb0390e50b9 (patch) | |
| tree | 58295927c3eee59886c6c81aec47538c226a1144 /test-suite/success | |
| parent | dc981a7262727395b0519ad2bbe43676bc665503 (diff) | |
| parent | 1bc80b5cf7792e13b9d793de2c8da5192c75920c (diff) | |
Merge PR #10318: Test goal range in "only" selectors
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite/success')
| -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. |