Modifying theories to preferably use the "[= ]" syntax, and,

sometimes, to use "intros [= ...]" rather than things like "intros H;
injection H as [= ...]".

Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>

14 files changed, 68 insertions, 72 deletions

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.