Add qualified names test

Author: dhalilov

test-suite/success/QualifiedGoalNames.v

@@ -0,0 +1,27 @@
+(* -*- mode: coq; coq-prog-args: ("-accessible-goal-names") -*- *)
+
+Goal forall a b : bool, a = a.
+Proof.
+  intros.
+  destruct a.
+  [true_case]: destruct b.
+  [true_case.true_case]: reflexivity.
+  [true_case.false_case]: reflexivity.
+  [false_case]: reflexivity.
+Qed.
+
+Goal forall a b c : bool, a = a.
+Proof.
+  intros.
+  destruct a.
+  all: destruct b.
+  all: destruct c.
+  [true_case.true_case.true_case]: reflexivity.
+  [true_case.true_case.false_case]: reflexivity.
+  [true_case.false_case.true_case]: reflexivity.
+  [true_case.false_case.false_case]: reflexivity.
+  [false_case.true_case.true_case]: reflexivity.
+  [false_case.true_case.false_case]: reflexivity.
+  [false_case.false_case.true_case]: reflexivity.
+  [false_case.false_case.false_case]: reflexivity.
+Qed.