2 files changed, 14 insertions, 3 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index c072cc641..8745cf2fb 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -4,6 +4,7 @@ Require Eqdep_dec.
 
 (* Check that Injection tries Intro until *)
 
+Unset Structural Injection.
 Lemma l1 : forall x : nat, S x = S (S x) -> False.
  injection 1.
 apply n_Sn.
@@ -37,6 +38,7 @@ intros.
  injection H.
 exact (fun H => H).
 Qed.
+Set Structural Injection.
 
 (* Test injection as *)
 
@@ -65,7 +67,7 @@ Qed.
 Goal (forall x y : nat, x = y -> S x = S y) -> True.
 intros.
 einjection (H O).
-instantiate (1:=O).
+2:instantiate (1:=O).
 Abort.
 
 Goal (forall x y : nat, x = y -> S x = S y) -> True.
@@ -85,12 +87,21 @@ Qed.
 (* Basic case, using sigT *)
 
 Scheme Equality for nat.
+Unset Structural Injection.
 Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
   existT P n H1 = existT P n H2 -> H1 = H2.
 intros.
 injection H.
 intro H0. exact H0.
 Abort.
+Set Structural Injection.
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  existT P n H1 = existT P n H2 -> H1 = H2.
+intros.
+injection H as H0.
+exact H0.
+Abort.
 
 (* Test injection using K, knowing that an equality is decidable *)
 (* Basic case, using sigT, with "as" clause *)
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 11fbf24d4..3f8a7f3eb 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -831,7 +831,7 @@ Proof.
  intro n.
  apply nat_ind with (P:= fun n => n <> S n).
  discriminate.
- red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
+ red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;auto.
 Qed.
 
 Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}.
@@ -1076,7 +1076,7 @@ Proof.
  simpl.
  destruct i; discriminate 1.
  destruct i; simpl;auto.
- injection 1; injection 2;intros; subst a; subst b; auto.
+ injection 1; injection 1; subst a; subst b; auto.
 Qed.
 
  Set Implicit Arguments.