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 00000000..ed035f52
--- /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.