diff options
| author | Cyprien Mangin | 2016-06-03 09:57:20 +0200 |
|---|---|---|
| committer | Cyprien Mangin | 2016-06-14 06:21:30 +0200 |
| commit | 9356f42d5f84f9b325f71bab041d1b8184384a21 (patch) | |
| tree | 15031e5d024e6925d65bcac5c8b0c3fd21b8b4be /test-suite | |
| parent | 1e19f163b8c7a21d63165784828f4d733aa95171 (diff) | |
Remove the need for brackets in goal selectors.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/goal_selector.v | 28 |
1 files changed, 18 insertions, 10 deletions
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index fc3c8a92db..9ba748e2a5 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -13,21 +13,29 @@ 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. - [2-5]:exact One. + 2, 4-99, 100-3:idtac. + 2-5:exact One. par:exact Zero. - repeat split. - [3-6]:swap 1 4. - [1-5]:swap 1 5. - [0-4]:exact One. + 3-6:swap 1 4. + 1-5:swap 1 5. + 0-4:exact One. all:exact Zero. - repeat split. - [1, 3]:exact Zero. - [1, 2, 3, 4]: exact One. + 1, 3:exact Zero. + 1, 2, 3, 4: exact One. - repeat split. all:apply transform. - [2, 4, 6]:apply transform. + 2, 4, 6:apply transform. all:apply transform. - [1-5]:apply transform. - [1-6]:exact One. + 1-5:apply transform. + 1-6:exact One. +Qed. + +Goal True -> True. +Proof. + intros y. + Fail 1-1:let x := y in idtac x. + 1:let x := y in idtac x. + exact I. Qed.
\ No newline at end of file |