4 files changed, 4 insertions, 4 deletions
diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index fd4bb248bf..904ee4dac1 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 7394cebdef..3646018719 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 8fcc077164..9c690e2b4a 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 760ad4da11..b69196679f 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.