7 files changed, 19 insertions, 20 deletions
diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v
index ced6d9594..79671ce93 100644
--- a/test-suite/bugs/closed/3068.v
+++ b/test-suite/bugs/closed/3068.v
@@ -56,7 +56,7 @@ Section Finite_nat_set.
       subst fs1.
       apply iff_refl.
     intros H.
-    eapply counted_list_equal_nth_char.
+    eapply (counted_list_equal_nth_char _ _ _ _ ?[def]).
     intros i.
     destruct (counted_def_nth fs1 i _ ) eqn:H0.
     (* This was not part of the initial bug report; this is to check that
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 52e1e0ed0..9680d2bbf 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 b1558dab1..26eaca827 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 c5a393408..576fbd7c0 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] 
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 8fd039462..56ed89ed8 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -70,7 +70,7 @@ Abort.
 
 Goal (forall x y : nat, x = y -> S x = S y) -> True.
 intros.
-einjection (H O) as H0.
+einjection (H O ?[y]) as H0.
 instantiate (y:=O).
 Abort.
 
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 55b666b72..02e043bc3 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -543,7 +543,7 @@ Qed.
 Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a):
   exists x, exists y, X x y.
 Proof.
-intros; eexists; eexists; case H.
+intros; eexists; eexists ?[y]; case H.
 apply (foo ?y).
 Grab Existential Variables.
 exact 0.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 9f091e399..90a60daa6 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -96,21 +96,21 @@ Abort.
 (* Check that subterm selection does not solve existing evars *)
 
 Goal exists x, S x = S 0.
-eexists.
+eexists ?[x].
 Show x.  (* Incidentally test Show on a named goal *)
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S 0).
 Abort.
 
 Goal exists x, S 0 = S x.
-eexists.
+eexists ?[x].
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S ?x).
 [x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *)
 Abort.
 
 Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
-do 2 eexists.
+eexists ?[n]; eexists ?[p].
 destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *)
 change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n).
 Abort.
@@ -426,7 +426,7 @@ destruct b eqn:H.
 (* Check natural instantiation behavior when the goal has already an evar *)
 
 Goal exists x, S x = x.
-eexists.
+eexists ?[x].
 destruct (S _).
 change (0 = ?x).
 Abort.