Catch up to where I was last time.

Many of the changes are a consequence of coq/coq#13132.

4 files changed, 7 insertions, 11 deletions

diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 9ff18ebe2c..d6a0ae5411 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -567,9 +567,7 @@ Section Normalize.
 
   Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m.
   Proof.
-    red in H, H0. red in H.
-    apply (snd (H _ _)). 
-    assumption.
+    apply (_ : Normalizes R0 R1). assumption.
   Qed.
 
   Lemma flip_atom R : Normalizes R (flip (flip R)).
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index c489d82d0b..561822ef0c 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -352,14 +352,12 @@ Section Binary.
   Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R.
   Proof with auto.
     reduce_goal.
-    apply H. firstorder.
+    firstorder.
   Qed.
 
   Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
   Proof.
-    unfold flip; constructor; unfold flip.
-    - intros X. apply H. apply symmetry. apply X.
-    - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption.
+    firstorder.
   Qed.
 End Binary.
 
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index d96bd72561..4d9069b4d0 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -64,8 +64,8 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1.
          now transitivity y.
   Qed.
 
-Arguments equiv_symmetric {A R} sa x y.
-Arguments equiv_transitive {A R} sa x y z.
+Arguments equiv_symmetric {A R} sa x y : rename.
+Arguments equiv_transitive {A R} sa x y z : rename.
 
 (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
 
diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v
index 515372466a..e4129f8382 100644
--- a/theories/micromega/Tauto.v
+++ b/theories/micromega/Tauto.v
@@ -1371,13 +1371,13 @@ Section S.
     destruct pol;auto.
     generalize (is_cnf_tt_inv (xcnf (negb true) f1)).
     destruct (is_cnf_tt (xcnf (negb true) f1)).
-    + intros.
+    + intros H.
       rewrite H by auto.
       reflexivity.
     +
       generalize (is_cnf_ff_inv (xcnf (negb true) f1)).
     destruct (is_cnf_ff (xcnf (negb true) f1)).
-    * intros.
+    * intros H.
       rewrite H by auto.
       unfold or_cnf_opt.
       simpl.