diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-16 13:34:46 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-16 13:34:46 +0100 |
| commit | b0ac9d9748440badec581a3a804caec09c6df49d (patch) | |
| tree | 73ff209532c950b2a83854ebc015a58cad864798 /test-suite/success | |
| parent | 8ea2a8307a8d96f8275ebbd9bd4cbd1f6b0a00c6 (diff) | |
| parent | 1856d60057ac9096c791d71d4282c0cdfef85913 (diff) | |
Merge PR #6551: Bracket with goal selector
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/BracketsWithGoalSelector.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v new file mode 100644 index 000000000..ed035f521 --- /dev/null +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -0,0 +1,16 @@ +Goal forall A B, B \/ A -> A \/ B. +Proof. + intros * [HB | HA]. + 2: { + left. + exact HA. + Fail right. (* No such goal. Try unfocusing with "}". *) + } + Fail 2: { (* Non-existent goal. *) + idtac. (* The idtac is to get a dot, so that IDEs know to stop there. *) + 1:{ (* Syntactic test: no space before bracket. *) + right. + exact HB. +Fail Qed. + } +Qed. |