diff options
Diffstat (limited to 'test-suite/output')
-rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
-rw-r--r-- | test-suite/output/Notations2.v | 5 |
2 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 6ff1d3837..13ed7816d 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -54,3 +54,5 @@ end : ∀ x : nat, x <= 0 -> {x0 : nat | x <= x0} exist (Q x) y conj : {x0 : A | Q x x0} +{1, 2} + : nat -> Prop diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 4e0d135d7..3f3945052 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -106,3 +106,8 @@ Check fun x (H:le x 0) => exist (le x) 0 H. Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y). Check (exist (Q x) y conj). + +(* 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}). |