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.

32 files changed, 163 insertions, 108 deletions

diff --git a/CHANGES b/CHANGES
index 12d486c42..e90d3d105 100644
--- a/CHANGES
+++ b/CHANGES
@@ -30,6 +30,11 @@ Tactics
 - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO).
 - New goal selectors.  Sets of goals can be selected by select by listing
   integers ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24.
+- For uniformity with "destruct"/"induction" and for a more natural
+  behavior, "injection" can now work in place by activating option
+  "Structural Injection". In this case, hypotheses are also put in the
+  context in the natural left-to-right order and the hypothesis on
+  which injection applies is cleared.
 
 Hints
 
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index 60ce59ed9..725f2a534 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -144,6 +144,10 @@ TACTIC EXTEND einjection_as
 | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
     [ mytclWithHoles (injClause (Some ipat)) true c ]
 END
+TACTIC EXTEND simple_injection
+| [ "simple" "injection" ] -> [ simpleInjClause false None ]
+| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles simpleInjClause false c ]
+END
 
 let injHyp id =
   Proofview.tclEVARMAP >>= fun sigma ->
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index fd4bb248b..904ee4dac 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -914,7 +914,7 @@ Qed.
  revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros.
  - discriminate.
  - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst.
-   * injection H; intros <-. rewrite <- PSubstL1_ok; intuition.
+   * injection H as <-. rewrite <- PSubstL1_ok; intuition.
    * now apply IH.
  Qed.
 
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index 7394cebde..364601871 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -266,7 +266,7 @@ Qed.
 
 Lemma push_not_empty: forall a S, (push a S) <> empty.
 intros a [ind cont];unfold push,empty.
-simpl;intro H;injection H; intros _ ; apply Pos.succ_not_1.
+intros [= H%Pos.succ_not_1]. assumption.
 Qed.
 
 Fixpoint In (x:A) (S:Store) (F:Full S) {struct F}: Prop :=
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 8fcc07716..9c690e2b4 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -96,7 +96,7 @@ Section ZMORPHISM.
  Proof.
   constructor.
   destruct c;intros;try discriminate.
-  injection H;clear H;intros H1;subst c'.
+  injection H as <-.
   simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
  Qed.
 
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 760ad4da1..b69196679 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -883,7 +883,7 @@ Section MakeRingPol.
  revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros.
  - discriminate.
  - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst.
-   * injection H; intros <-. rewrite <- PSubstL1_ok; intuition.
+   * injection H as <-. rewrite <- PSubstL1_ok; intuition.
    * now apply IH.
  Qed.
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index db7d2e4a1..1d3239ef6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -72,11 +72,26 @@ let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
-      optname  = "injection left-to-right pattern order";
+      optname  = "injection left-to-right pattern order and clear by default when with introduction pattern";
       optkey   = ["Injection";"L2R";"Pattern";"Order"];
       optread  = (fun () -> !injection_pattern_l2r_order) ;
       optwrite = (fun b -> injection_pattern_l2r_order := b) }
 
+let injection_in_context = ref false
+
+let use_injection_in_context () =
+  !injection_in_context
+  && Flags.version_strictly_greater Flags.V8_5
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "injection in context";
+      optkey   = ["Structural";"Injection"];
+      optread  = (fun () -> !injection_in_context) ;
+      optwrite = (fun b -> injection_in_context := b) }
+
 (* Rewriting tactics *)
 
 let tclNOTSAMEGOAL tac =
@@ -1381,27 +1396,41 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
       inject_at_positions env sigma l2r u eq_clause posns
 	(tac (clenv_value eq_clause))
 
-let use_clear_hyp_by_default () = false
-
-let postInjEqTac with_evars clear_flag ipats c n =
-  match ipats with
-  | Some ipats ->
-      let clear_tac =
-        let dft =
-          use_injection_pattern_l2r_order () || use_clear_hyp_by_default () in
-        tclTRY (apply_clear_request clear_flag dft c) in
-      let intro_tac =
-        if use_injection_pattern_l2r_order ()
-        then intro_patterns_bound_to with_evars n MoveLast ipats
-        else intro_patterns_to with_evars MoveLast ipats in
-      tclTHEN clear_tac intro_tac
-  | None -> apply_clear_request clear_flag false c
-
-let injEq with_evars clear_flag ipats =
-  let l2r =
-    if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false
+let get_previous_hyp_position id gl =
+  let rec aux dest = function
+  | [] -> raise (RefinerError (NoSuchHyp id))
+  | d :: right ->
+    let hyp = Context.Named.Declaration.get_id d in
+    if Id.equal hyp id then dest else aux (MoveAfter hyp) right
   in
-  injEqThen (fun c i -> postInjEqTac with_evars clear_flag ipats c i) l2r
+  aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
+
+let injEq ?(old=false) with_evars clear_flag ipats =
+  (* Decide which compatibility mode to use *)
+  let ipats_style, l2r, dft_clear_flag, bounded_intro = match ipats with
+    | None when not old && use_injection_in_context () ->
+      Some [], true, true, true
+    | None -> None, false, false, false
+    | _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in
+  (* Built the post tactic depending on compatibility mode *)
+  let post_tac c n =
+    match ipats_style with
+    | Some ipats ->
+      Proofview.Goal.enter { enter = begin fun gl ->
+        let destopt = match kind_of_term c with
+        | Var id -> get_previous_hyp_position id gl
+        | _ -> MoveLast in
+        let clear_tac =
+          tclTRY (apply_clear_request clear_flag dft_clear_flag c) in
+        (* Try should be removal if dependency were treated *)
+        let intro_tac =
+          if bounded_intro
+          then intro_patterns_bound_to with_evars n destopt ipats
+          else intro_patterns_to with_evars destopt ipats in
+        tclTHEN clear_tac intro_tac
+      end }
+    | None -> tclIDTAC in
+  injEqThen post_tac l2r
 
 let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats)
 
@@ -1409,6 +1438,10 @@ let injClause ipats with_evars = function
   | None -> onNegatedEquality with_evars (injEq with_evars None ipats)
   | Some c -> onInductionArg (inj ipats with_evars) c
 
+let simpleInjClause with_evars = function
+  | None -> onNegatedEquality with_evars (injEq ~old:true with_evars None None)
+  | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c
+
 let injConcl = injClause None false None
 let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 1122615c3..47cb6b82f 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -79,6 +79,8 @@ val injClause    : intro_patterns option -> evars_flag ->
   constr with_bindings destruction_arg option -> unit Proofview.tactic
 val injHyp       : clear_flag -> Id.t -> unit Proofview.tactic
 val injConcl     : unit Proofview.tactic
+val simpleInjClause : evars_flag ->
+  constr with_bindings destruction_arg option -> unit Proofview.tactic
 
 val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
 val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v
index 13ec5bea9..536e6fabd 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 e598e5aed..5df92998e 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 29496be5e..bef3c33ca 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/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.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 340a79689..f8020a50e 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 3fc74943e..d6d370cb5 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 eaeb2914b..9a227ad13 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 9e59f0c50..b1c0fdaa2 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 7398c6d65..507f1cda6 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 59fdbb42f..a3eb91ec6 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 b66699220..9886ae6a8 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 8dd240f46..be95a0379 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 751d4f35c..83a2343dd 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 c115a831d..04fc5a8df 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 56cb9bbc2..7c76011f2 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 8673b8a58..63fb5800c 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 ec1017f50..e8ff516f3 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 0ccfad7b2..7baf102aa 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 17f05c511..a349eb908 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 6bfa47bc5..9f9651d84 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 8470b7955..44f8ff6a7 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 943bb48e9..451b65cbe 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 4b8447f49..b2ada2f91 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.