1 files changed, 22 insertions, 4 deletions
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 57d8ebbc..e902a3c2 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -25,19 +25,25 @@ 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.
 
+(* Test notation for anonymous functions up to eta-expansion *)
+
+Check fun P:nat->nat->Prop => fun x:nat => ex (P x). 
+
 (* Test notations with binders *)
 
-Notation "∃  x .. y , P":=
-  (ex (fun x => .. (ex (fun y => P)) ..)) (x binder, y binder, at level 200).
+Notation "∃  x .. y , P":= (ex (fun x => .. (ex (fun y => P)) ..))
+  (x binder, y binder, at level 200, right associativity).
 
 Check (∃ n p, n+p=0).
 
+Check ∃ (a:=0) (x:nat) y (b:=1) (c:=b) (d:=2) z (e:=3) (f:=4), x+y = z+d.
+
 Notation "∀  x .. y , P":= (forall x, .. (forall y, P) ..)
   (x binder, at level 200, right associativity).
 
 Check (∀ n p, n+p=0).
 
-Notation "'λ'  x .. y , P":= (fun x, .. (fun y, P) ..)
+Notation "'λ'  x .. y , P":= (fun x => .. (fun y => P) ..)
   (y binder, at level 200, right associativity).
 
 Check (λ n p, n+p=0).
@@ -53,7 +59,19 @@ Notation "'let'' f x .. y  :=  t 'in' u":=
   (f ident, x closed binder, y closed binder, at level 200,
    right associativity).
 
-Check let' f x y z (a:bool) := x+y+z+1 in f 0 1 2.
+Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
+
+(* In practice, only the printing rule is used here *)
+(* Note: does not work for pattern *)
+Notation "f ( x )" := (f x) (at level 10, format "f ( x )").
+Check fun f x => f x + S x.
+
+Open Scope list_scope.
+Notation list1 := (1::nil)%list.
+Notation plus2 n := (S (S n)).
+(* plus2 was not correctly printed in the two following tests in 8.3pl1 *)
+Print plus2.
+Check fun n => match n with list1 => 0 | _ => 2 end.
 
 (* This one is not fully satisfactory because binders in the same type
    are re-factorized and parentheses are needed even for atomic binder