diff options
Diffstat (limited to 'test-suite')
| -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 3b3351d330..cf45025ea4 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -10,6 +10,8 @@ end : nat let '(a, _, _) := (2, 3, 4) in a : nat +exists myx (y : bool), myx = y + : Prop fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0 : (nat -> nat -> Prop) -> nat -> Prop ∃ n p : nat, n + p = 0 diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 1fcbe858a8..e53c94ef0a 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -25,6 +25,11 @@ Remove Printing Let prod. Check match (0,0,0) with (x,y,z) => x+y+z end. Check let '(a,b,c) := ((2,3),4) in a. +(* Check printing of notations with mixed reserved binders (see bug #2571) *) + +Implicit Type myx : bool. +Check exists myx y, myx = y. + (* Test notation for anonymous functions up to eta-expansion *) Check fun P:nat->nat->Prop => fun x:nat => ex (P x). |