5 files changed, 46 insertions, 4 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 139f9e99..7c9b1e27 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -91,3 +91,11 @@ The simpl tactic unfolds f
   when the 5th, 6th and 7th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.f
+forall w : r, w 3 true = tt
+     : Prop
+The command has indeed failed with message:
+=> Error: Unknown interpretation for notation "$".
+w 3 true = tt
+     : Prop
+The command has indeed failed with message:
+=> Error: Extra argument _.
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 3a94f19a..573cfdab 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -38,3 +38,15 @@ End S1.
 About f.
 Arguments f : clear implicits and scopes.
 About f.
+Record r := { pi :> nat -> bool -> unit }.
+Notation "$" := 3 (only parsing) : foo_scope.
+Notation "$" := true (only parsing) : bar_scope.
+Delimit Scope bar_scope with B.
+Arguments pi _ _%F _%B. 
+Check (forall w : r, pi w $ $ = tt).
+Fail Check (forall w : r, w $ $ = tt).
+Axiom w : r.
+Arguments w  _%F _%B : extra scopes.
+Check (w $ $ = tt).
+Fail Arguments w  _%F _%B.
+
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 47741e43..cf45025e 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
@@ -46,3 +48,7 @@ match n with
 | plus2 _ :: _ => 2
 end
      : list(nat) -> nat
+# x : nat => x
+     : nat -> nat
+# _ : nat => 2
+     : nat -> nat
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.
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 40c786ab..598bb728 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -37,10 +37,11 @@ When applied to no arguments:
 When applied to 1 argument:
   Argument A is implicit
 plus = 
-fix plus (n m : nat) : nat := match n with
-                              | 0 => m
-                              | S p => S (plus p m)
-                              end
+fix plus (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (plus p m)
+  end
      : nat -> nat -> nat
 
 Argument scopes are [nat_scope nat_scope]