2 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 20101f48e5..5541ccf57b 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -58,3 +58,5 @@ exist (Q x) y conj
      : nat -> nat
 % j
      : nat -> nat
+{1, 2}
+     : nat -> Prop
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 3cf89818d9..1d8278c088 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -111,3 +111,8 @@ Check (exist (Q x) y conj).
 Notation "% i" := (fun i : nat => i) (at level 0, i ident).
 Check %i.
 Check %j.
+
+(* Check bug raised on coq-club on Sep 12, 2016 *)
+
+Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))).
+Check ({1, 2}).