Merge branch 'v8.5'

3 files changed, 12 insertions, 13 deletions

diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 52e1e0ed01..9680d2bbff 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1,5 +1,4 @@
-Existential 1 =
-?Goal1 : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
+Existential 1 = ?Goal : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
 Existential 2 =
 ?y : [p : nat  q := S p : nat  n : nat  m : nat |- nat] (p, q cannot be used)
 Existential 3 = ?Goal0 : [q : nat  n : nat  m : nat |- n = ?y] 
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b1558dab1c..26eaca8272 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,14 +111,14 @@ fun x : option Z => match x with
                     | NONE2 => 0
                     end
      : option Z -> Z
-fun x : list ?T1 => match x with
-                    | NIL => NONE2
-                    | (_ :') t => SOME2 t
-                    end
-     : list ?T1 -> option (list ?T1)
+fun x : list ?T => match x with
+                   | NIL => NONE2
+                   | (_ :') t => SOME2 t
+                   end
+     : list ?T -> option (list ?T)
 where
-?T1 : [x : list ?T1  x1 : list ?T1  x0 := x1 : list ?T1 |- Type] (x, x1,
-      x0 cannot be used)
+?T : [x : list ?T  x1 : list ?T  x0 := x1 : list ?T |- Type] (x, x1,
+     x0 cannot be used)
 s
      : s
 10
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index c5a393408e..576fbd7c0b 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -9,10 +9,10 @@ fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
 fun n : nat => let x := A n : T n in ?y ?y0 : T n
      : forall n : nat, T n
 where
-?y : [n : nat  x := A n : T n |- ?T0 -> T n] 
-?y0 : [n : nat  x := A n : T n |- ?T0] 
+?y : [n : nat  x := A n : T n |- ?T -> T n] 
+?y0 : [n : nat  x := A n : T n |- ?T] 
 fun n : nat => ?y ?y0 : T n
      : forall n : nat, T n
 where
-?y : [n : nat |- ?T0 -> T n] 
-?y0 : [n : nat |- ?T0] 
+?y : [n : nat |- ?T -> T n] 
+?y0 : [n : nat |- ?T]