diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-01-15 13:54:01 +0100 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-01-15 14:18:49 +0100 |
| commit | 1856d60057ac9096c791d71d4282c0cdfef85913 (patch) | |
| tree | f8b33554b85c09ce9792eca55a7e74bf6f3d7362 /test-suite/success | |
| parent | 54083a2a8e6c4c2083717ac18c7b4dc351ab0f7d (diff) | |
More tests on brackets with goal selectors (including failures).
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/BracketsWithGoalSelector.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v index dd032767c..ed035f521 100644 --- a/test-suite/success/BracketsWithGoalSelector.v +++ b/test-suite/success/BracketsWithGoalSelector.v @@ -4,7 +4,13 @@ Proof. 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. } - right. - exact HB. Qed. |