Giving a more natural semantics to injection by default.

There were three versions of injection:

1. "injection term" without "as" clause:
   was leaving hypotheses on the goal in reverse order
2. "injection term as ipat", first version:
   was introduction hypotheses using ipat in reverse order without
   checking that the number of ipat was the size of the injection
   (activated with "Unset Injection L2R Pattern Order")
3. "injection term as ipat", second version:
   was introduction hypotheses using ipat in left-to-right order
   checking that the number of ipat was the size of the injection
   and clearing the injecting term by default if an hypothesis
   (activated with "Set Injection L2R Pattern Order", default one from 8.5)

There is now:

4. "injection term" without "as" clause, new version:
   introducing the components of the injection in the context in
   left-to-right order using default intro-patterns "?"
   and clearing the injecting term by default if an hypothesis
   (activated with "Set Structural Injection")

The new versions 3. and 4. are the "expected" ones in the sense that
they have the following good properties:
- introduction in the context is in the natural left-to-right order
- "injection" behaves the same with and without "as", always
  introducing the hypotheses in the goal what corresponds to the
  natural expectation as the changes I made in the proof scripts for
  adaptation confirm
- clear the "injection" hypothesis when an hypothesis which is the
  natural expectation as the changes I made in the proof scripts for
  adaptation confirm

The compatibility can be preserved by "Unset Structural Injection" or
by calling "simple injection".

The flag is currently off.

19 files changed, 72 insertions, 78 deletions

diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 340a796891..f8020a50e0 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -38,8 +38,7 @@ intros m n.
 generalize (eq_refl (S n)).
 generalize n at -1.
 induction (S n) as [|n0 IHn0]; try discriminate.
-clear n; intros n H; injection H; clear H; intro H.
-rewrite <- H; intros le_mn1 le_mn2; clear n H.
+clear n; intros n [= <-] le_mn1 le_mn2.
 pose (def_n2 := eq_refl n0); transitivity (eq_ind _ _ le_mn2 _ def_n2).
   2: reflexivity.
 generalize def_n2; revert le_mn1 le_mn2.
@@ -50,7 +49,7 @@ destruct le_mn1; intros le_mn2; destruct le_mn2.
   now destruct (Nat.nle_succ_diag_l _ le_mn0).
 + intros def_n0; generalize le_mn1; rewrite def_n0; intros le_mn0.
   now destruct (Nat.nle_succ_diag_l _ le_mn0).
-+ intros def_n0; injection def_n0; intros ->.
++ intros def_n0. injection def_n0 as ->.
   rewrite (UIP_nat _ _ def_n0 eq_refl); simpl.
   assert (H : le_mn1 = le_mn2).
     now apply IHn0.
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 3fc74943e1..d6d370cb51 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -14,3 +14,4 @@
 
 Global Unset Bracketing Last Introduction Pattern.
 Global Unset Regular Subst Tactic.
+Global Unset Structural Injection.
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index eaeb2914b3..9a227ad130 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -1986,7 +1986,7 @@ Module OrdProperties (M:S).
   simpl; intros; try discriminate.
   intros.
   destruct a; destruct l; simpl in *.
-  injection H; clear H; intros; subst.
+  injection H as -> ->.
   inversion_clear H1.
   red in H; simpl in *; intuition.
   elim H0; eauto.
@@ -2050,10 +2050,10 @@ Module OrdProperties (M:S).
   generalize (elements_3 m).
   destruct (elements m).
   try discriminate.
-  destruct p; injection H; intros; subst.
-  inversion_clear H1.
+  destruct p; injection H as -> ->; intros H4.
+  inversion_clear H1 as [? ? H2|? ? H2].
   red in H2; destruct H2; simpl in *; ME.order.
-  inversion_clear H4.
+  inversion_clear H4. rename H1 into H3.
   rewrite (@InfA_alt _ eqke) in H3; eauto with *.
   apply (H3 (y,x0)); auto.
   Qed.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 9e59f0c505..b1c0fdaa2f 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -274,8 +274,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         rewrite append_assoc_1; apply in_or_app; right; apply in_cons;
           apply IHm2; auto.
         rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
-        rewrite append_neutral_r; apply in_or_app; injection H;
-          intro EQ; rewrite EQ; right; apply in_eq.
+        rewrite append_neutral_r; apply in_or_app; injection H as ->;
+          right; apply in_eq.
         rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto.
         rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
         congruence.
@@ -315,7 +315,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
          apply in_or_app.
         left; apply IHm1; auto.
         right; destruct (in_inv H0).
-         injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq.
+         injection H1 as -> ->; apply in_eq.
          apply in_cons; apply IHm2; auto.
         left; apply IHm1; auto.
         right; apply IHm2; auto.
@@ -346,7 +346,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
          apply in_or_app.
         left; apply IHm1; auto.
         right; destruct (in_inv H0).
-         injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq.
+         injection H1 as -> ->; apply in_eq.
          apply in_cons; apply IHm2; auto.
         left; apply IHm1; auto.
         right; apply IHm2; auto.
@@ -689,7 +689,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst.
   red; red; simpl.
   destruct H0.
-  injection H0; clear H0; intros _ H0; subst.
+  injection H0 as H0 _; subst.
   eapply xelements_bits_lt_1; eauto.
   apply E.bits_lt_trans with p.
   eapply xelements_bits_lt_1; eauto.
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index 7398c6d654..507f1cda69 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -1007,10 +1007,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       destruct o.
         intros x H. injection H; intros; subst. reflexivity.
         revert IHl. case choose.
-          intros p Hp x H. injection H; intros; subst; clear H. apply Hp.
+          intros p Hp x H. injection H as <-. apply Hp.
            reflexivity.
           intros _ x. revert IHr. case choose.
-            intros p Hp H. injection H; intros; subst; clear H. apply Hp.
+            intros p Hp H. injection H as <-. apply Hp.
             reflexivity.
             intros. discriminate.
   Qed.
@@ -1066,11 +1066,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
    induction s as [| l IHl o r IHr]; simpl.
      intros. discriminate.
      intros x. destruct (min_elt l); intros.
-       injection H. intros <-. apply IHl. reflexivity.
+       injection H as <-. apply IHl. reflexivity.
        destruct o; simpl.
-         injection H. intros <-. reflexivity.
+         injection H as <-. reflexivity.
          destruct (min_elt r); simpl in *.
-           injection H. intros <-. apply IHr. reflexivity.
+           injection H as <-. apply IHr. reflexivity.
            discriminate.
   Qed.
 
@@ -1094,15 +1094,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; intros x y H H'.
       discriminate.
       simpl in H. case_eq (min_elt l).
-        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        intros p Hp. rewrite Hp in H. injection H as <-.
         destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial.
         intro Hp; rewrite Hp in H. apply min_elt_3 in Hp.
         destruct o.
-          injection H. intros <- Hl. clear H.
+          injection H as <-. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (min_elt r).
-            injection H. intros <-. clear H.
+            injection H as <-.
             destruct y as [z|z|].
               apply (IHr e z); trivial.
               elim (Hp _ H').
@@ -1119,11 +1119,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
    induction s as [| l IHl o r IHr]; simpl.
      intros. discriminate.
      intros x. destruct (max_elt r); intros.
-       injection H. intros <-. apply IHr. reflexivity.
+       injection H as <-. apply IHr. reflexivity.
        destruct o; simpl.
-         injection H. intros <-. reflexivity.
+         injection H as <-. reflexivity.
          destruct (max_elt l); simpl in *.
-           injection H. intros <-. apply IHl. reflexivity.
+           injection H as <-. apply IHl. reflexivity.
            discriminate.
   Qed.
 
@@ -1147,15 +1147,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; intros x y H H'.
       discriminate.
       simpl in H. case_eq (max_elt r).
-        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        intros p Hp. rewrite Hp in H. injection H as <-.
         destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial.
         intro Hp; rewrite Hp in H. apply max_elt_3 in Hp.
         destruct o.
-          injection H. intros <- Hl. clear H.
+          injection H as <-. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (max_elt l).
-            injection H. intros <-. clear H.
+            injection H as <-.
             destruct y as [z|z|].
               elim (Hp _ H').
               apply (IHl e z); trivial.
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 59fdbb42f0..a3eb91ec65 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -79,7 +79,7 @@ Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x.
 
 (* use either discriminate or injection on a hypothesis *)
 
-Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)).
+Ltac destr_eq H := discriminate H || (try (injection H as H)).
 
 (* Similar variants of destruct *)
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index b666992206..9886ae6a8e 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -248,8 +248,7 @@ Section Facts.
     generalize (app_nil_r l); intros E.
     rewrite -> E; auto.
     intros.
-    injection H.
-    intro.
+    injection H as H H0.
     assert ([] = l ++ a0 :: l0) by auto.
     apply app_cons_not_nil in H1 as [].
   Qed.
@@ -335,7 +334,7 @@ Section Facts.
     absurd (length (x1 :: l1 ++ l) <= length l).
     simpl; rewrite app_length; auto with arith.
     rewrite H; auto with arith.
-    injection H; clear H; intros; f_equal; eauto.
+    injection H as H H0; f_equal; eauto.
   Qed.
 
 End Facts.
@@ -518,7 +517,7 @@ Section Elts.
   Proof.
     revert l.
     induction n as [|n IH]; intros [|x l] H; simpl in *; try easy.
-    - exists nil; exists l. injection H; clear H; intros; now subst.
+    - exists nil; exists l. now injection H as ->.
     - destruct (IH _ H) as (l1 & l2 & H1 & H2).
       exists (x::l1); exists l2; simpl; split; now f_equal.
   Qed.
@@ -1385,9 +1384,8 @@ End Fold_Right_Recursor.
     Lemma combine_split : forall (l:list A)(l':list B), length l = length l' ->
       split (combine l l') = (l,l').
     Proof.
-      induction l; destruct l'; simpl; intros; auto; try discriminate.
-      injection H; clear H; intros.
-      rewrite IHl; auto.
+      induction l, l'; simpl; trivial; try discriminate.
+      now intros [= ->%IHl].
     Qed.
 
     Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B),
@@ -1471,7 +1469,7 @@ End Fold_Right_Recursor.
       destruct (in_app_or _ _ _ H); clear H.
       destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_).
       destruct (H1 H0) as (z,(H2,H3)); clear H0 H1.
-      injection H2; clear H2; intros; subst; intuition.
+      injection H2 as -> ->; intuition.
       intuition.
     Qed.
 
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index 8dd240f46e..be95a03799 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -908,10 +908,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       destruct o.
         intros x H. injection H; intros; subst. reflexivity.
         revert IHl. case choose.
-          intros p Hp x H. injection H; intros; subst; clear H. apply Hp.
+          intros p Hp x H. injection H as <-. apply Hp.
            reflexivity.
           intros _ x. revert IHr. case choose.
-            intros p Hp H. injection H; intros; subst; clear H. apply Hp.
+            intros p Hp H. injection H as <-. apply Hp.
             reflexivity.
             intros. discriminate.
   Qed.
@@ -968,11 +968,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
    induction s as [| l IHl o r IHr]; simpl.
      intros. discriminate.
      intros x. destruct (min_elt l); intros.
-       injection H. intros <-. apply IHl. reflexivity.
+       injection H as <-. apply IHl. reflexivity.
        destruct o; simpl.
-         injection H. intros <-. reflexivity.
+         injection H as <-. reflexivity.
          destruct (min_elt r); simpl in *.
-           injection H. intros <-. apply IHr. reflexivity.
+           injection H as <-. apply IHr. reflexivity.
            discriminate.
   Qed.
 
@@ -996,15 +996,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; intros x y H H'.
       discriminate.
       simpl in H. case_eq (min_elt l).
-        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        intros p Hp. rewrite Hp in H. injection H as <-.
         destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial.
         intro Hp; rewrite Hp in H. apply min_elt_spec3 in Hp.
         destruct o.
-          injection H. intros <- Hl. clear H.
+          injection H as <-. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (min_elt r).
-            injection H. intros <-. clear H.
+            injection H as <-.
             destruct y as [z|z|].
               apply (IHr e z); trivial.
               elim (Hp _ H').
@@ -1021,11 +1021,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
    induction s as [| l IHl o r IHr]; simpl.
      intros. discriminate.
      intros x. destruct (max_elt r); intros.
-       injection H. intros <-. apply IHr. reflexivity.
+       injection H as <-. apply IHr. reflexivity.
        destruct o; simpl.
-         injection H. intros <-. reflexivity.
+         injection H as <-. reflexivity.
          destruct (max_elt l); simpl in *.
-           injection H. intros <-. apply IHl. reflexivity.
+           injection H as <-. apply IHl. reflexivity.
            discriminate.
   Qed.
 
@@ -1049,15 +1049,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; intros x y H H'.
       discriminate.
       simpl in H. case_eq (max_elt r).
-        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        intros p Hp. rewrite Hp in H. injection H as <-.
         destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial.
         intro Hp; rewrite Hp in H. apply max_elt_spec3 in Hp.
         destruct o.
-          injection H. intros <- Hl. clear H.
+          injection H as <-. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (max_elt l).
-            injection H. intros <-. clear H.
+            injection H as <-.
             destruct y as [z|z|].
               elim (Hp _ H').
               apply (IHl e z); trivial.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index 751d4f35c6..83a2343dd4 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -911,7 +911,7 @@ Proof.
      { inversion_clear O.
        assert (InT x l) by now apply min_elt_spec1. auto. }
      simpl. case X.compare_spec; try order.
-     destruct lc; injection E; clear E; intros; subst l s0; auto.
+     destruct lc; injection E; subst l s0; auto.
 Qed.
 
 Lemma remove_min_spec1 s x s' `{Ok s}:
@@ -1948,7 +1948,7 @@ Module Make (X: Orders.OrderedType) <:
  generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs).
  set (P := Raw.remove_min_ok s). clearbody P.
  destruct (Raw.remove_min s) as [(x0,s0)|]; try easy.
- intros H U. injection U. clear U; intros; subst. simpl.
+ intros H U. injection U as -> <-. simpl.
  destruct (H x s0); auto. subst; intuition.
  Qed.
 
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index c115a831d9..04fc5a8dfa 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -369,7 +369,7 @@ Section ZModulo.
  assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)).
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l).
- destruct 1; injection H; clear H; intros.
+ destruct 1; injection H as ? ?.
  rewrite H0.
  assert ([|l|] = l).
   apply Zmod_small; auto.
@@ -411,7 +411,7 @@ Section ZModulo.
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod [|a|] [|b|] H0).
  destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H1; clear H1; intros.
+ injection H1 as ? ?.
  assert ([|r|]=r).
   apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
    auto with zarith.
@@ -522,7 +522,7 @@ Section ZModulo.
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod a [|b|] H3).
  destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H4; clear H4; intros.
+ injection H4 as ? ?.
  assert ([|r|]=r).
   apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
    auto with zarith.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 56cb9bbc2c..7c76011f21 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -138,7 +138,7 @@ intros NEQ.
 generalize (BigZ.spec_div_eucl a b).
 generalize (Z_div_mod_full [a] [b] NEQ).
 destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r').
-intros (EQ,_). injection 1. intros EQr EQq.
+intros (EQ,_). injection 1 as EQr EQq.
 BigZ.zify. rewrite EQr, EQq; auto.
 Qed.
 
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 8673b8a58f..63fb5800c1 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -427,13 +427,13 @@ Module Make (NN:NType) <: ZType.
  (* Pos Neg *)
  generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr;
+ try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr;
       simpl; rewrite Hq, NN.spec_0; auto).
  change (- Zpos py) with (Zneg py).
  assert (GT : Zpos py > 0) by (compute; auto).
  generalize (Z_div_mod (Zpos px) (Zpos py) GT).
  unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r').
- intros (EQ,MOD). injection 1. intros Hr' Hq'.
+ intros (EQ,MOD). injection 1 as Hq' Hr'.
  rewrite NN.spec_eqb, NN.spec_0, Hr'.
  break_nonneg r pr EQr.
  subst; simpl. rewrite NN.spec_0; auto.
@@ -442,13 +442,13 @@ Module Make (NN:NType) <: ZType.
  (* Neg Pos *)
  generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr;
+ try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr;
       simpl; rewrite Hq, NN.spec_0; auto).
  change (- Zpos px) with (Zneg px).
  assert (GT : Zpos py > 0) by (compute; auto).
  generalize (Z_div_mod (Zpos px) (Zpos py) GT).
  unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r').
- intros (EQ,MOD). injection 1. intros Hr' Hq'.
+ intros (EQ,MOD). injection 1 as Hq' Hr'.
  rewrite NN.spec_eqb, NN.spec_0, Hr'.
  break_nonneg r pr EQr.
  subst; simpl. rewrite NN.spec_0; auto.
@@ -457,7 +457,7 @@ Module Make (NN:NType) <: ZType.
  (* Neg Neg *)
  generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto).
+ try (injection 1 as -> ->; auto).
  simpl. intros <-; auto.
  Qed.
 
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index ec1017f505..e8ff516f35 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -110,7 +110,7 @@ intros NEQ.
 generalize (BigN.spec_div_eucl a b).
 generalize (Z_div_mod_full [a] [b] NEQ).
 destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r').
-intros (EQ,_). injection 1. intros EQr EQq.
+intros (EQ,_). injection 1 as EQr EQq.
 BigN.zify. rewrite EQr, EQq; auto.
 Qed.
 
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 0ccfad7b28..7baf102aaa 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -201,7 +201,6 @@ Proof.
 Qed.
 
 (** ** No neutral elements for addition *)
-
 Lemma add_no_neutral p q : q + p <> p.
 Proof.
   revert q.
@@ -508,7 +507,7 @@ Qed.
 Lemma mul_xO_discr p q : p~0 * q <> q.
 Proof.
   induction q; try discriminate.
-  rewrite mul_xO_r; injection; assumption.
+  rewrite mul_xO_r; injection; auto.
 Qed.
 
 (** ** Simplification properties of multiplication *)
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 17f05c5113..a349eb9085 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -333,7 +333,7 @@ Ltac simplify_one_dep_elim_term c :=
       (let hyp := fresh in intros hyp ;
         move hyp before y ; revert_until hyp ; generalize dependent y ;
           refine (solution_right _ _ _ _)(*  ; intros until 0 *))
-    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
+    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; simple injection H; clear H)
     | ?t = ?u -> _ => let hyp := fresh in
       intros hyp ; exfalso ; discriminate
     | ?x = ?y -> _ => let hyp := fresh in
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 6bfa47bc55..9f9651d84a 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -84,7 +84,7 @@ Arguments Q2Qc q%Q.
 Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'.
 Proof.
  split; intro H.
- - injection H. apply Qred_eq_iff.
+ - now injection H as H%Qred_eq_iff.
  - apply Qc_is_canon. simpl. now rewrite H.
 Qed.
 
@@ -266,7 +266,7 @@ Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0.
 Proof.
   intros.
   destruct (Qmult_integral x y); try qc; auto.
-  injection H; clear H; intros.
+  injection H as H.
   rewrite <- (Qred_correct (x*y)).
   rewrite <- (Qred_correct 0).
   rewrite H; auto with qarith.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 8470b79550..44f8ff6a71 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -318,7 +318,7 @@ Lemma Permutation_length_2_inv :
 Proof.
   intros a1 a2 l H; remember [a1;a2] as m in H.
   revert a1 a2 Heqm.
-  induction H; intros; try (injection Heqm; intros; subst; clear Heqm);
+  induction H; intros; try (injection Heqm as ? ?; subst);
     discriminate || (try tauto).
   apply Permutation_length_1_inv in H as ->; left; auto.
   apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as [];
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 943bb48e92..451b65cbe9 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -83,7 +83,7 @@ intros H; generalize (H 0); simpl; intros H1; inversion H1.
 case (Rec s).
 intros H0; rewrite H0; auto.
 intros n; exact (H (S n)).
-intros H; injection H; intros H1 H2 n; case n; auto.
+intros H; injection H as H1 H2.
 rewrite H2; trivial.
 rewrite H1; auto.
 Qed.
@@ -238,14 +238,14 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl;
  auto.
 intros n; case n; simpl; auto.
 intros m s1; case s1; simpl; auto.
-intros H; injection H; intros H1; rewrite <- H1; auto.
+intros H; injection H as <-; auto.
 intros; discriminate.
 intros; discriminate.
 intros b s2' Rec n m s1.
 case n; simpl; auto.
 generalize (prefix_correct s1 (String b s2'));
  case (prefix s1 (String b s2')).
-intros H0 H; injection H; intros H1; rewrite <- H1; auto.
+intros H0 H; injection H as <-; auto.
 case H0; simpl; auto.
 case m; simpl; auto.
 case (index 0 s1 s2'); intros; discriminate.
@@ -271,7 +271,7 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl;
  auto.
 intros n; case n; simpl; auto.
 intros m s1; case s1; simpl; auto.
-intros H; injection H; intros H1; rewrite <- H1.
+intros H; injection H as <-.
 intros p H0 H2; inversion H2.
 intros; discriminate.
 intros; discriminate.
@@ -279,7 +279,7 @@ intros b s2' Rec n m s1.
 case n; simpl; auto.
 generalize (prefix_correct s1 (String b s2'));
  case (prefix s1 (String b s2')).
-intros H0 H; injection H; intros H1; rewrite <- H1; auto.
+intros H0 H; injection H as <-; auto.
 intros p H2 H3; inversion H3.
 case m; simpl; auto.
 case (index 0 s1 s2'); intros; discriminate.
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 4b8447f496..b2ada2f919 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -44,14 +44,11 @@ Section WfLexicographic_Product.
     apply H2.
     auto with sets.
 
-    injection H1.
-    destruct 2.
-    injection H3.
-    destruct 2; auto with sets.
+    injection H1 as <- _.
+    injection H3 as <- _; auto with sets.
 
     rewrite <- H1.
-    injection H3; intros _ Hx1.
-    subst x1.
+    injection H3 as -> H3.
     apply IHAcc0.
     elim inj_pair2 with A B x y' x0; assumption.
   Defined.