Merge PR #9288: Giving preference to syntax "injection ... as [= pat1 ... patn]".

Reviewed-by: Zimmi48

22 files changed, 124 insertions, 82 deletions

diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst
new file mode 100644
index 0000000000..6a74551f06
--- /dev/null
+++ b/doc/changelog/04-tactics/09288-injection-as.rst
@@ -0,0 +1,4 @@
+- Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as
+  an alternative to :n:`injection @term as {+ @simple_intropattern}` using
+  the standard :n:`@injection_intropattern` syntax (`#09288
+  <https://github.com/coq/coq/pull/09288>`_, by Hugo Herbelin).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 67d32835f5..fa6d62ffa2 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -131,16 +131,17 @@ include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`.
    simple_intropattern_closed : `naming_intropattern`
                               : _
                               : `or_and_intropattern`
-                              : `equality_intropattern`
+                              : `rewriting_intropattern`
+                              : `injection_intropattern`
    naming_intropattern     : `ident`
                            : ?
                            : ?`ident`
    or_and_intropattern     : [ `intropattern_list` | ... | `intropattern_list` ]
                            : ( `simple_intropattern` , ... , `simple_intropattern` )
                            : ( `simple_intropattern` & ... & `simple_intropattern` )
-   equality_intropattern   : ->
+   rewriting_intropattern  : ->
                            : <-
-                           : [= `intropattern_list` ]
+   injection_intropattern  : [= `intropattern_list` ]
    or_and_intropattern_loc : `or_and_intropattern`
                            : `ident`
 
@@ -2285,6 +2286,18 @@ and an explanation of the underlying technique.
       to the number of new equalities. The original equality is erased if it
       corresponds to a hypothesis.
 
+   .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern
+             injection @num as @injection_intropattern
+             injection as @injection_intropattern
+             einjection @term {? with @bindings_list} as @injection_intropattern
+             einjection @num as @injection_intropattern
+             einjection as @injection_intropattern
+
+      These are equivalent to the previous variants but using instead the
+      syntax :token:`injection_intropattern` which :tacn:`intros`
+      uses. In particular :n:`as [= {+ @simple_intropattern}]` behaves
+      the same as :n:`as {+ @simple_intropattern}`.
+
    .. flag:: Structural Injection
 
       This option ensure that :n:`injection @term` erases the original hypothesis
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index f5098d2a34..4c186dce09 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -146,6 +146,23 @@ let discrHyp id =
 let injection_main with_evars c =
  elimOnConstrWithHoles (injClause None None) with_evars c
 
+let isInjPat pat = match pat.CAst.v with IntroAction (IntroInjection _) -> Some pat.CAst.loc | _ -> None
+
+let decode_inj_ipat ?loc = function
+  (* For the "as [= pat1 ... patn ]" syntax *)
+  | [{ CAst.v = IntroAction (IntroInjection ipat) }] -> ipat
+  (* For the "as pat1 ... patn" syntax *)
+  | ([] | [_]) as ipat -> ipat
+  | pat1::pat2::_ as ipat ->
+  (* To be sure that there is no confusion of syntax, we check that no [= ...] occurs
+     in the non-singleton list of patterns *)
+  match isInjPat pat1 with
+  | Some _ -> user_err ?loc:pat2.CAst.loc (str "Unexpected pattern.")
+  | None ->
+  match List.map_filter isInjPat ipat with
+  | loc :: _ -> user_err ?loc (str "Unexpected injection pattern.")
+  | [] -> ipat
+
 }
 
 TACTIC EXTEND injection
@@ -158,15 +175,15 @@ TACTIC EXTEND einjection
 END
 TACTIC EXTEND injection_as
 | [ "injection" "as" intropattern_list(ipat)] ->
-    { injClause None (Some ipat) false None }
+    { injClause None (Some (decode_inj_ipat ipat)) false None }
 | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] ->
-    { mytclWithHoles (injClause None (Some ipat)) false c }
+    { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) false c }
 END
 TACTIC EXTEND einjection_as
 | [ "einjection" "as" intropattern_list(ipat)] ->
-    { injClause None (Some ipat) true None }
+    { injClause None (Some (decode_inj_ipat ipat)) true None }
 | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] ->
-    { mytclWithHoles (injClause None (Some ipat)) true c }
+    { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) true c }
 END
 TACTIC EXTEND simple_injection
 | [ "simple" "injection" ] -> { simpleInjClause None false None }
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 36ed0210e3..b20f45af3e 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -925,7 +925,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 as <-. rewrite <- PSubstL1_ok; intuition.
+   * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition.
    * now apply IH.
  Qed.
 
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 4886c8b9aa..9be2535a3f 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -105,7 +105,7 @@ Section ZMORPHISM.
  Proof.
   constructor.
   destruct c;intros;try discriminate.
-  injection H as <-.
+  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 f7cb6b688b..c5d396427b 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -894,7 +894,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 as <-. rewrite <- PSubstL1_ok; intuition.
+   * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition.
    * now apply IH.
  Qed.
 
diff --git a/test-suite/output/injection.out b/test-suite/output/injection.out
new file mode 100644
index 0000000000..ff40a478f3
--- /dev/null
+++ b/test-suite/output/injection.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+Unexpected pattern.
+The command has indeed failed with message:
+Unexpected injection pattern.
diff --git a/test-suite/output/injection.v b/test-suite/output/injection.v
new file mode 100644
index 0000000000..bfd5a67bf5
--- /dev/null
+++ b/test-suite/output/injection.v
@@ -0,0 +1,8 @@
+(* Test error messages *)
+
+Goal forall x, (x,0) = (0, S x) -> x = 0.
+Fail intros x H; injection H as [= H'] H''.
+Fail intros x H; injection H as H' [= H''].
+intros x H; injection H as [= H' H''].
+exact H'.
+Qed.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index ddbc128aa1..6a4a0445b5 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -53,7 +53,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 as ->.
++ 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/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index e68bc5930d..153842654a 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -1988,7 +1988,7 @@ Module OrdProperties (M:S).
   simpl; intros; try discriminate.
   intros.
   destruct a; destruct l; simpl in *.
-  injection H as -> ->.
+  injection H as [= -> ->].
   inversion_clear H1.
   red in H; simpl in *; intuition.
   elim H0; eauto.
@@ -2052,7 +2052,7 @@ Module OrdProperties (M:S).
   generalize (elements_3 m).
   destruct (elements m).
   try discriminate.
-  destruct p; injection H as -> ->; intros H4.
+  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. rename H1 into H3.
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index b47c99244b..37dd2304da 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -277,7 +277,7 @@ 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 as ->;
+        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.
@@ -318,7 +318,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
          apply in_or_app.
         left; apply IHm1; auto.
         right; destruct (in_inv H0).
-         injection H1 as -> ->; apply in_eq.
+         injection H1 as [= -> ->]; apply in_eq.
          apply in_cons; apply IHm2; auto.
         left; apply IHm1; auto.
         right; apply IHm2; auto.
@@ -349,7 +349,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
          apply in_or_app.
         left; apply IHm1; auto.
         right; destruct (in_inv H0).
-         injection H1 as -> ->; apply in_eq.
+         injection H1 as [= -> ->]; apply in_eq.
          apply in_cons; apply IHm2; auto.
         left; apply IHm1; auto.
         right; apply IHm2; auto.
@@ -692,7 +692,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 as 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 8a93f38164..d2e10e42a6 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -1009,10 +1009,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 as <-. apply Hp.
+          intros p Hp x [= <-]. apply Hp.
            reflexivity.
           intros _ x. revert IHr. case choose.
-            intros p Hp H. injection H as <-. apply Hp.
+            intros p Hp [= <-]. apply Hp.
             reflexivity.
             intros. discriminate.
   Qed.
@@ -1068,11 +1068,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 as <-. apply IHl. reflexivity.
+       injection H as [= <-]. apply IHl. reflexivity.
        destruct o; simpl.
-         injection H as <-. reflexivity.
+         injection H as [= <-]. reflexivity.
          destruct (min_elt r); simpl in *.
-           injection H as <-. apply IHr. reflexivity.
+           injection H as [= <-]. apply IHr. reflexivity.
            discriminate.
   Qed.
 
@@ -1096,15 +1096,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 as <-.
+        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 as <-. intros Hl.
+          injection H as [= <-]. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (min_elt r).
-            injection H as <-.
+            injection H as [= <-].
             destruct y as [z|z|].
               apply (IHr e z); trivial.
               elim (Hp _ H').
@@ -1121,11 +1121,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 as <-. apply IHr. reflexivity.
+       injection H as [= <-]. apply IHr. reflexivity.
        destruct o; simpl.
-         injection H as <-. reflexivity.
+         injection H as [= <-]. reflexivity.
          destruct (max_elt l); simpl in *.
-           injection H as <-. apply IHl. reflexivity.
+           injection H as [= <-]. apply IHl. reflexivity.
            discriminate.
   Qed.
 
@@ -1149,15 +1149,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 as <-.
+        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 as <-. intros Hl.
+          injection H as [= <-]. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (max_elt l).
-            injection H as <-.
+            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 497cf2550b..7eb717787e 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -75,7 +75,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 as 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 a48e9929c4..f73440eb1a 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -250,7 +250,7 @@ Section Facts.
     generalize (app_nil_r l); intros E.
     rewrite -> E; auto.
     intros.
-    injection H as H H0.
+    injection H as [= H H0].
     assert ([] = l ++ a0 :: l0) by auto.
     apply app_cons_not_nil in H1 as [].
   Qed.
@@ -261,18 +261,14 @@ Section Facts.
     induction x as [| x l IHl];
       [ destruct y as [| a l] | destruct y as [| a l0] ];
       simpl; auto.
-    - intros a b H.
-      injection H.
+    - intros a b [= ].
       auto.
-    - intros a0 b H.
-      injection H as H1 H0.
+    - intros a0 b [= H1 H0].
       apply app_cons_not_nil in H0 as [].
-    - intros a b H.
-      injection H as H1 H0.
+    - intros a b [= H1 H0].
       assert ([] = l ++ [a]) by auto.
       apply app_cons_not_nil in H as [].
-    - intros a0 b H.
-      injection H as <- H0.
+    - intros a0 b [= <- H0].
       destruct (IHl l0 a0 b H0) as (<-,<-).
       split; auto.
   Qed.
@@ -336,7 +332,7 @@ Section Facts.
     absurd (length (x1 :: l1 ++ l) <= length l).
     simpl; rewrite app_length; auto with arith.
     rewrite H; auto with arith.
-    injection H as H H0; f_equal; eauto.
+    injection H as [= H H0]; f_equal; eauto.
   Qed.
 
 End Facts.
@@ -519,7 +515,7 @@ Section Elts.
   Proof.
     revert l.
     induction n as [|n IH]; intros [|x l] H; simpl in *; try easy.
-    - exists nil; exists l. now injection H as ->.
+    - 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.
@@ -1243,7 +1239,7 @@ End Fold_Right_Recursor.
     Proof.
      induction l as [|a l IH]; simpl; [easy| ].
      case_eq (f a); intros Ha Eq.
-     * injection Eq as ->; auto.
+     * injection Eq as [= ->]; auto.
      * destruct (IH Eq); auto.
     Qed.
 
@@ -1304,10 +1300,10 @@ End Fold_Right_Recursor.
     forall x:A, In x l <-> In x l1 \/ In x l2.
   Proof.
     revert l1 l2. induction l as [| a l' Hrec]; simpl; intros l1 l2 Eq x.
-    - injection Eq as <- <-. tauto.
+    - injection Eq as [= <- <-]. tauto.
     - destruct (partition l') as (left, right).
       specialize (Hrec left right eq_refl x).
-      destruct (f a); injection Eq as <- <-; simpl; tauto.
+      destruct (f a); injection Eq as [= <- <-]; simpl; tauto.
   Qed.
 
   End Bool.
@@ -1483,7 +1479,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 as -> ->; intuition.
+      injection H2 as [= -> ->]; intuition.
       intuition.
     Qed.
 
diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v
index c9822f47dc..13f63c5cbc 100644
--- a/theories/Logic/WeakFan.v
+++ b/theories/Logic/WeakFan.v
@@ -64,7 +64,7 @@ induction l1, l2.
 - discriminate.
 - discriminate.
 - intros H (HY1,H1) (HY2,H2).
-  injection H as H.
+  injection H as [= H].
   pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1.
   subst l1.
   f_equal.
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index a726eebd31..330c7959ac 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -910,10 +910,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 as <-. apply Hp.
+          intros p Hp x [= <-]. apply Hp.
            reflexivity.
           intros _ x. revert IHr. case choose.
-            intros p Hp H. injection H as <-. apply Hp.
+            intros p Hp [= <-]. apply Hp.
             reflexivity.
             intros. discriminate.
   Qed.
@@ -970,11 +970,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 as <-. apply IHl. reflexivity.
+       injection H as [= <-]. apply IHl. reflexivity.
        destruct o; simpl.
-         injection H as <-. reflexivity.
+         injection H as [= <-]. reflexivity.
          destruct (min_elt r); simpl in *.
-           injection H as <-. apply IHr. reflexivity.
+           injection H as [= <-]. apply IHr. reflexivity.
            discriminate.
   Qed.
 
@@ -998,15 +998,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 as <-.
+        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 as <-. intros Hl.
+          injection H as [= <-]. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (min_elt r).
-            injection H as <-.
+            injection H as [= <-].
             destruct y as [z|z|].
               apply (IHr e z); trivial.
               elim (Hp _ H').
@@ -1023,11 +1023,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 as <-. apply IHr. reflexivity.
+       injection H as [= <-]. apply IHr. reflexivity.
        destruct o; simpl.
-         injection H as <-. reflexivity.
+         injection H as [= <-]. reflexivity.
          destruct (max_elt l); simpl in *.
-           injection H as <-. apply IHl. reflexivity.
+           injection H as [= <-]. apply IHl. reflexivity.
            discriminate.
   Qed.
 
@@ -1051,15 +1051,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 as <-.
+        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 as <-. intros Hl.
+          injection H as [= <-]. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (max_elt l).
-            injection H as <-.
+            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 f9105fdf74..a2ffd2050e 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -1950,7 +1950,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 as -> <-. simpl.
+ intros H [= -> <-]. 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 4bcd22543f..94da55b3f3 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -372,7 +372,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 as ? ?.
+ destruct 1; injection H as [= ? ?].
  rewrite H0.
  assert ([|l|] = l).
   apply Zmod_small; auto.
@@ -414,7 +414,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 as ? ?.
+ injection H1 as [= ? ?].
  assert ([|r|]=r).
   apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
    auto with zarith.
@@ -525,7 +525,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 as ? ?.
+ 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/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index f18fca99a0..9eae960086 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -43,10 +43,10 @@ Proof.
   generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)).
   rewrite <- Z.ggcd_gcd.
   destruct Z.ggcd as (g,(aa,bb)); simpl in *.
-  injection H as <- <-. intros H (_,H').
+  injection H as [= <- <-]. intros H (_,H').
   destruct g as [|g|g]; [ discriminate | | now elim H ].
   destruct bb as [|b|b]; simpl in *; try discriminate.
-  injection H' as H'. f_equal.
+  injection H' as [= H']. f_equal.
   apply Pos.mul_reg_r with b. now rewrite Pos.mul_1_l.
 Qed.
 
@@ -87,7 +87,7 @@ Arguments Q2Qc q%Q.
 Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'.
 Proof.
  split; intro H.
- - now injection H as H%Qred_eq_iff.
+ - now injection H as [= H%Qred_eq_iff].
  - apply Qc_is_canon. simpl. now rewrite H.
 Qed.
 
@@ -269,7 +269,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 as H.
+  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 f5bc9eee4e..170c221a45 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -304,7 +304,7 @@ Qed.
 Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a].
 Proof.
   intros a l H; remember [a] as m in H.
-  induction H; try (injection Heqm as -> ->);
+  induction H; try (injection Heqm as [= -> ->]);
     discriminate || auto.
   apply Permutation_nil in H as ->; trivial.
 Qed.
@@ -312,7 +312,7 @@ Qed.
 Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b.
 Proof.
   intros a b H.
-  apply Permutation_length_1_inv in H; injection H as ->; trivial.
+  apply Permutation_length_1_inv in H; injection H as [= ->]; trivial.
 Qed.
 
 Lemma Permutation_length_2_inv :
@@ -320,7 +320,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 as ? ?; subst);
+  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 [];
@@ -332,7 +332,7 @@ Lemma Permutation_length_2 :
     a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
 Proof.
   intros a1 b1 a2 b2 H.
-  apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto.
+  apply Permutation_length_2_inv in H as [H|H]; injection H as [= -> ->]; auto.
 Qed.
 
 Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' ->
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 08ccfac877..85bde6a4df 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -123,7 +123,7 @@ intros H; generalize (H O); simpl; intros H1; inversion H1.
 case (Rec s).
 intros H0; rewrite H0; auto.
 intros n; exact (H (S n)).
-intros H; injection H as H1 H2.
+intros [= H1 H2].
 rewrite H2; trivial.
 rewrite H1; auto.
 Qed.
@@ -290,14 +290,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 as <-; auto.
+intros [= <-]; 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 as <-; auto.
+intros H0 [= <-]; auto.
 case H0; simpl; auto.
 case m; simpl; auto.
 case (index O s1 s2'); intros; discriminate.
@@ -323,7 +323,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 as <-.
+intros [= <-].
 intros p H0 H2; inversion H2.
 intros; discriminate.
 intros; discriminate.
@@ -331,7 +331,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 as <-; auto.
+intros H0 [= <-]; 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 b2d08186ea..60db536dce 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -46,11 +46,11 @@ Section WfLexicographic_Product.
           apply H2.
           auto with sets.
 
-      + injection H1 as <- _.
-        injection H3 as <- _; auto with sets.
+      + injection H1 as [= <- _].
+        injection H3 as [= <- _]; auto with sets.
 
     - rewrite <- H1.
-      injection H3 as -> H3.
+      injection H3 as [= -> H3].
       apply IHAcc0.
       elim inj_pair2 with A B x y' x0; assumption.
   Defined.