Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index e902a3c2..e53c94ef 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). 
@@ -83,3 +88,13 @@ Notation "'mylet' f [ x ; .. ; y ]  :=  t 'in' u":=
 
 Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
 *)
+
+(* Check notations for functional terms which do not necessarily
+   depend on their parameter *)
+(* Old request mentioned again on coq-club 20/1/2012 *)
+
+Notation "#  x : T => t" := (fun x : T => t)
+  (at level 0, t at level 200, x ident).
+
+Check # x : nat => x.
+Check # _ : nat => 2.