diff options
| -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. |