2 files changed, 11 insertions, 4 deletions
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 783b30c0fc..2e0e145e1a 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -14,6 +14,11 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
      : (nat -> nat -> Prop) -> nat -> Prop
 ∃ n p : nat, n + p = 0
      : Prop
+∃ x y : nat,
+let b := 1 in
+let c := b in
+let d := 2 in ∃ z : nat, let e := 3 in let f := 4 in x + y = z + d
+     : Prop
 ∀ n p : nat, n + p = 0
      : Prop
 λ n p : nat, n + p = 0
@@ -25,7 +30,7 @@ fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
 λ A : Type, ∀ n p : A, n = p
      : Type -> Prop
 Defining 'let'' as keyword
-let' f (x y z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2
+let' f (x y : nat) (a:=0) (z : nat) (_ : bool) := x + y + z + 1 in (f(0)) 1 2
      : bool -> nat
 λ (f : nat -> nat) (x : nat), f(x) + S(x)
      : (nat -> nat) -> nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 4f9b9ccc7b..e902a3c273 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -31,11 +31,13 @@ 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).
 
@@ -57,7 +59,7 @@ 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 *)