7 files changed, 30 insertions, 11 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 4d59a92cbf..f4ecfd7362 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -98,5 +98,10 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
      : nat -> Prop
 tele (t : Type) '(y, z) (x : t0) := tt
      : forall t : Type, nat * nat -> t -> fpack
+[fun x : nat => x + 0;; fun x : nat => x + 1;; fun x : nat => x + 2]
+     : (nat -> nat) *
+       ((nat -> nat) *
+        ((nat -> nat) *
+         ((nat -> nat) * ((nat -> nat) * ((nat -> nat) * (nat -> nat))))))
 foo5 x nat x
      : nat -> nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 96d831944f..71536c68fb 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -140,6 +140,12 @@ Notation "'tele' x .. z := b" :=
 
 Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
 
+(* Checking that "fun" in a notation does not mixed up with the
+   detection of a recursive binder *)
+
+Notation "[ x ;; .. ;; y ]" := ((x,((fun u => S u), .. (y,(fun u => S u,fun v:nat => v)) ..))).
+Check [ fun x => x+0 ;; fun x => x+1 ;; fun x => x+2 ].
+
 (* Cyprien's part of bug #4765 *)
 
 Notation foo5 x T y := (fun x : T => y).
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
index bf1bf2809d..ca56f032ff 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -1,12 +1,10 @@
-3 subgoals (ID 29)
+3 subgoals (ID 31)
   
   H : 0 = 0
   ============================
   1 = 1
 
-subgoal 2 (ID 33) is:
+subgoal 2 (ID 35) is:
  1 = S (S m')
-subgoal 3 (ID 20) is:
+subgoal 3 (ID 22) is:
  S (S n') = S m
-
-(dependent evars: (printing disabled) )
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index c70467912f..d28ee42761 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x : T n := A n in ?t ?y : T n
+fun n : nat => let y : T n := A n in ?t ?x : T n
      : forall n : nat, T n
 where
-?t : [n : nat  x := A n : T n |- ?T -> T n] 
-?y : [n : nat  x := A n : T n |- ?T] 
-fun n : nat => ?t ?y : T n
+?t : [n : nat  y := A n : T n |- ?T -> T n] 
+?x : [n : nat  y := A n : T n |- ?T] 
+fun n : nat => ?t ?x : T n
      : forall n : nat, T n
 where
 ?t : [n : nat |- ?T -> T n] 
-?y : [n : nat |- ?T] 
+?x : [n : nat |- ?T] 
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 1825db1676..f761a4dc5a 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -27,5 +27,5 @@ Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
 (* Note: exact numbers of evars are not important... *)
 
 Inductive T (n:nat) : Type := A : T n.
-Check fun n (x:=A n:T n) => _ _ : T n.
+Check fun n (y:=A n:T n) => _ _ : T n.
 Check fun n => _ _ : T n.
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index 9471b892dd..48be63a46a 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -3,3 +3,9 @@ In environment
 y : nat
 The term "a y" has type "{y0 : nat | y = y0}"
 while it is expected to have type "{x : nat | x = y}".
+1 focused subgoal
+(shelved: 1)
+  
+  H : ?n <= 3 -> 3 <= ?n -> ?n = 3
+  ============================
+  True
diff --git a/test-suite/output/names.v b/test-suite/output/names.v
index b3b5071a03..f1efd0df2a 100644
--- a/test-suite/output/names.v
+++ b/test-suite/output/names.v
@@ -3,3 +3,7 @@
 
 Parameter a : forall x, {y:nat|x=y}.
 Fail Definition b y : {x:nat|x=y} := a y.
+
+Goal (forall n m, n <= m -> m <= n -> n = m) -> True.
+intro H; epose proof (H _ 3) as H.
+Show.