7 files changed, 34 insertions, 10 deletions
diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v
index 13ec5bea9b..536e6fabd9 100644
--- a/test-suite/bugs/closed/2016.v
+++ b/test-suite/bugs/closed/2016.v
@@ -1,6 +1,8 @@
 (* Coq 8.2beta4 *)
 Require Import Classical_Prop. 
 
+Unset Structural Injection.
+
 Record coreSemantics : Type := CoreSemantics {
   core: Type;
   corestep: core ->  core -> Prop;
@@ -49,7 +51,7 @@ unfold oe_corestep; intros.
 assert (HH:= step_fun _ _ _ H H0); clear H H0.
 destruct q1; destruct q2; unfold oe2coreSem; simpl in *.
 generalize (inj_pairT1 _ _ _ _ _ _ HH); clear HH; intros.
-injection H; clear H; intros.
+injection H.
 revert in_q1  in_corestep1 in_corestep_fun1
           H.
 pattern in_core1.
@@ -59,4 +61,4 @@ apply sym_eq.
 (** good to here **)
 Show Universes.
 Print Universes.
-Fail apply H0.
-\ No newline at end of file
+Fail apply H0.
diff --git a/test-suite/bugs/closed/2021.v b/test-suite/bugs/closed/2021.v
index e598e5aed7..5df92998e1 100644
--- a/test-suite/bugs/closed/2021.v
+++ b/test-suite/bugs/closed/2021.v
@@ -1,6 +1,8 @@
 (* correct failure of injection/discriminate on types whose inductive
    status derives from the substitution of an argument *)
 
+Unset Structural Injection.
+
 Inductive t : nat -> Type :=
 | M : forall n: nat, nat -> t n.
 
diff --git a/test-suite/bugs/closed/HoTT_coq_047.v b/test-suite/bugs/closed/HoTT_coq_047.v
index 29496be5ee..bef3c33ca1 100644
--- a/test-suite/bugs/closed/HoTT_coq_047.v
+++ b/test-suite/bugs/closed/HoTT_coq_047.v
@@ -1,3 +1,5 @@
+Unset Structural Injection.
+
 Inductive nCk : nat -> nat -> Type :=
   |zz : nCk 0 0
   | incl { m n : nat } : nCk m n -> nCk (S m) (S n)
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 21a8cf9ede..21554e9ff8 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -16,9 +16,8 @@ The command has indeed failed with message:
 In nested Ltac calls to "f2", "f1" and "refine", last call failed.
 The term "I" has type "True" while it is expected to have type "False".
 The command has indeed failed with message:
-Ltac call to "h" failed.
-Error: Ltac variable x is bound to I which cannot be coerced to
-a declared or quantified hypothesis.
+In nested Ltac calls to "h" and "injection", last call failed.
+Error: No primitive equality found.
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection", last call failed.
 Error: No primitive equality found.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 56ed89ed86..8745cf2fbd 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 *)
@@ -124,7 +135,7 @@ intros * [= H].
 exact H.
 Abort.
 
-(* Injection does not projects at positions in Prop... allow it?
+(* Injection does not project at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.
 Goal forall p q : True\/True, c _ p = c _ q -> False.
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 11fbf24d4d..d8f8042465 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}.
@@ -1075,8 +1075,8 @@ Proof.
  apply vector_double_rect.
  simpl.
  destruct i; discriminate 1.
- destruct i; simpl;auto.
- injection 1; injection 2;intros; subst a; subst b; auto.
+ destruct i; simpl;auto. 
+ injection 1 as ->; injection 1 as ->; auto.
 Qed.
 
  Set Implicit Arguments.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 3faa1ca43a..fba05cd902 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -64,3 +64,11 @@ assert (H:=H I).
 match goal with H:_ |- _ => clear H end.
 match goal with H:_ |- _ => exact H end.
 Qed.
+
+(* Test specialize as *)
+
+Goal (forall x, x=0) -> 1=0.
+intros.
+specialize (H 1) as ->.
+reflexivity.
+Qed.