6 files changed, 123 insertions, 36 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 924030ba..215d9b68 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -46,6 +46,32 @@ fun x : nat => ifn x is succ n then n else 0
      : bool
 -4
      : Z
+The command has indeed failed with message:
+=> Error: x should not be bound in a recursive pattern of the right-hand side.
+The command has indeed failed with message:
+=> Error: in the right-hand side, y and z should appear in
+   term position as part of a recursive pattern.
+The command has indeed failed with message:
+=> Error: The reference w was not found in the current environment.
+The command has indeed failed with message:
+=> Error: x is unbound in the right-hand side.
+The command has indeed failed with message:
+=> Error: in the right-hand side, y and z should appear in
+   term position as part of a recursive pattern.
+The command has indeed failed with message:
+=> Error: z is expected to occur in binding position in the right-hand side.
+The command has indeed failed with message:
+=> Error: as y is a non-closed binder, no such "," is allowed to occur.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Cannot find where the recursive pattern starts.
+The command has indeed failed with message:
+=> Error: Both ends of the recursive pattern are the same.
 SUM (nat * nat) nat
      : Set
 FST (0; 1)
@@ -59,6 +85,8 @@ Defining 'I' as keyword
      : Prop
 [|1, 2, 3; 4, 5, 6|]
      : Z * Z * Z * (Z * Z * Z)
+[|0 * (1, 2, 3); (4, 5, 6) * false|]
+     : Z * Z * (Z * Z) * (Z * Z) * (Z * bool * (Z * bool) * (Z * bool))
 fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
      : (Z -> Z -> Z -> Z) -> Z
 plus
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index f041b9b7..b8f8f48f 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -121,6 +121,39 @@ Notation "- 4" := (-2 + -2).
 Check -4.
 
 (**********************************************************************)
+(* Check ill-formed recursive notations *)
+
+(* Recursive variables not part of a recursive pattern *)
+Fail Notation "( x , y , .. , z )" := (pair x .. (pair y z) ..).
+
+(* No recursive notation *)
+Fail Notation "( x , y , .. , z )" := (pair x (pair y z)).
+
+(* Left-unbound variable *)
+Fail Notation "( x , y , .. , z )" := (pair x .. (pair y w) ..).
+
+(* Right-unbound variable *)
+Fail Notation "( x , y , .. , z )" := (pair y .. (pair z 0) ..).
+
+(* Not the right kind of recursive pattern *)
+Fail Notation "( x , y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..)).
+Fail Notation "( x -- y , .. , z )" := (pair y .. (pair z 0) ..)
+  (y closed binder, z closed binder).
+
+(* No separator allowed with open binders *)
+Fail Notation "( x -- y , .. , z )" := (ex (fun z => .. (ex (fun y => x)) ..))
+  (y binder, z binder).
+
+(* Ends of pattern do not match *)
+Fail Notation "( x , y , .. , z )" := (pair y .. (pair (plus z) 0) ..).
+Fail Notation "( x , y , .. , z )" := (pair y .. (plus z 0) ..).
+Fail Notation "( x1 , x2 , y , .. , z )" := (y y .. (x2 z 0) ..).
+Fail Notation "( x1 , x2 , y , .. , z )" := (x1 y .. (x2 z 0) ..).
+
+(* Ends of pattern are the same *)
+Fail Notation "( x , y , .. , z )" := (pair .. (pair (pair y z) x) .. x).
+
+(**********************************************************************)
 (* Check preservation of scopes at printing time *)
 
 Notation SUM := sum.
@@ -163,6 +196,12 @@ Notation "[| x , y , .. , z ; a , b , .. , c |]" :=
   (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)).
 Check [|1,2,3;4,5,6|].
 
+Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
+  (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z))
+        (pair .. (pair (pair a u) (pair b u)) .. (pair c u)))
+  (t at level 39).
+Check [|0*(1,2,3);(4,5,6)*false|].
+
 (**********************************************************************)
 (* Test recursive notations involving applications                    *)
 (* Caveat: does not work for applied constant because constants are   *)
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 20d20d82..6731d505 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -10,3 +10,18 @@ end
      : nat
 let '(a, _, _) := (2, 3, 4) in a
      : nat
+∃ n p : nat, n + p = 0
+     : Prop
+∀ n p : nat, n + p = 0
+     : Prop
+λ n p : nat, n + p = 0
+     : nat -> nat -> Prop
+λ (A : Type) (n p : A), n = p
+     : ∀ A : Type, A -> A -> Prop
+λ A : Type, ∃ n p : A, n = p
+     : Type -> Prop
+λ 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
+     : bool -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 2e136edf..57d8ebbc 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -24,3 +24,44 @@ Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x.
 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 notations with binders *)
+
+Notation "∃  x .. y , P":=
+  (ex (fun x => .. (ex (fun y => P)) ..)) (x binder, y binder, at level 200).
+
+Check (∃ n p, n+p=0).
+
+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) ..)
+  (y binder, at level 200, right associativity).
+
+Check (λ n p, n+p=0).
+
+Generalizable Variable A.
+
+Check `(λ n p : A, n=p).
+Check `(∃ n p : A, n=p).
+Check `(∀ n p : A, n=p).
+
+Notation "'let'' f x .. y  :=  t 'in' u":=
+  (let f := fun x => .. (fun 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.
+
+(* This one is not fully satisfactory because binders in the same type
+   are re-factorized and parentheses are needed even for atomic binder
+
+Notation "'mylet' f [ x ; .. ; y ]  :=  t 'in' u":=
+  (let f := fun x => .. (fun y => t) .. in u)
+  (f ident, x closed binder, y closed binder, at level 200,
+   right associativity).
+
+Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
+*)
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 99e736dd..154d9cdd 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -2,29 +2,11 @@ le_S: forall n m : nat, n <= m -> n <= S m
 le_n: forall n : nat, n <= n
 false: bool
 true: bool
-sumor_beq:
-  forall (A : Type) (B : Prop),
-  (A -> A -> bool) -> (B -> B -> bool) -> A + {B} -> A + {B} -> bool
-sumbool_beq:
-  forall A B : Prop,
-  (A -> A -> bool) -> (B -> B -> bool) -> {A} + {B} -> {A} + {B} -> bool
 xorb: bool -> bool -> bool
-sum_beq:
-  forall A B : Type,
-  (A -> A -> bool) -> (B -> B -> bool) -> A + B -> A + B -> bool
-prod_beq:
-  forall A B : Type,
-  (A -> A -> bool) -> (B -> B -> bool) -> A * B -> A * B -> bool
 orb: bool -> bool -> bool
-option_beq: forall A : Type, (A -> A -> bool) -> option A -> option A -> bool
 negb: bool -> bool
-nat_beq: nat -> nat -> bool
-list_beq: forall A : Type, (A -> A -> bool) -> list A -> list A -> bool
 implb: bool -> bool -> bool
-comparison_beq: comparison -> comparison -> bool
-bool_beq: bool -> bool -> bool
 andb: bool -> bool -> bool
-Empty_set_beq: Empty_set -> Empty_set -> bool
 pred_Sn: forall n : nat, n = pred (S n)
 plus_n_Sm: forall n m : nat, S (n + m) = n + S m
 plus_n_O: forall n : nat, n = n + 0
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 1a87f4cc..c87eaadc 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,28 +1,10 @@
 false: bool
 true: bool
-sumor_beq:
-  forall (A : Type) (B : Prop),
-  (A -> A -> bool) -> (B -> B -> bool) -> A + {B} -> A + {B} -> bool
-sumbool_beq:
-  forall A B : Prop,
-  (A -> A -> bool) -> (B -> B -> bool) -> {A} + {B} -> {A} + {B} -> bool
 xorb: bool -> bool -> bool
-sum_beq:
-  forall A B : Type,
-  (A -> A -> bool) -> (B -> B -> bool) -> A + B -> A + B -> bool
-prod_beq:
-  forall A B : Type,
-  (A -> A -> bool) -> (B -> B -> bool) -> A * B -> A * B -> bool
 orb: bool -> bool -> bool
-option_beq: forall A : Type, (A -> A -> bool) -> option A -> option A -> bool
 negb: bool -> bool
-nat_beq: nat -> nat -> bool
-list_beq: forall A : Type, (A -> A -> bool) -> list A -> list A -> bool
 implb: bool -> bool -> bool
-comparison_beq: comparison -> comparison -> bool
-bool_beq: bool -> bool -> bool
 andb: bool -> bool -> bool
-Empty_set_beq: Empty_set -> Empty_set -> bool
 S: nat -> nat
 O: nat
 pred: nat -> nat