No more `Typeclasses Opaque` for `equiv`.

theories/base.v

@@ -191,7 +191,11 @@ Proof. split; repeat intro; congruence. Qed.
 "canonical" equivalence for a type. The typeclass is tied to the \equiv
 symbol. This is based on (Spitters/van der Weegen, 2011). *)
 Class Equiv A := equiv: relation A.
-Typeclasses Opaque equiv.
+
+(* No Typeclasses Opaque because we often rely on [≡] being unified with [=] in
+case of types with Leibniz equality as [≡].
+Typeclasses Opaque equiv.  *)
+
 (* No Hint Mode set because of Coq bug #5735
 Hint Mode Equiv ! : typeclass_instances. *)
 
@@ -239,8 +243,6 @@ Ltac unfold_leibniz := repeat
   end.
 
 Definition equivL {A} : Equiv A := (=).
-Instance equivL_equivalence {A} : Equivalence (@equiv A equivL).
-Proof. unfold equiv; apply _. Qed.
 
 (** A [Params f n] instance forces the setoid rewriting mechanism not to
 rewrite in the first [n] arguments of the function [f]. We will declare such
@@ -663,14 +665,12 @@ Section prod_relation.
 End prod_relation.
 
 Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation (≡) (≡).
-Instance pair_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡) ==> (≡)) (@pair A B).
-Proof. apply pair_proper'. Qed.
-Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B).
-Proof. apply pair_inj'. Qed.
-Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B).
-Proof. apply fst_proper'. Qed.
-Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B).
-Proof. apply snd_proper'. Qed.
+Instance pair_proper `{Equiv A, Equiv B} :
+  Proper ((≡) ==> (≡) ==> (≡)) (@pair A B) := _.
+Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B) := _.
+Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := _.
+Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _.
+Typeclasses Opaque prod_equiv.
 
 Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B).
 Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed.
@@ -724,14 +724,11 @@ Section sum_relation.
 End sum_relation.
 
 Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡).
-Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B).
-Proof. apply inl_proper'. Qed.
-Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B).
-Proof. apply inr_proper'. Qed.
-Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B).
-Proof. apply inl_inj'. Qed.
+Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B) := _.
+Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B) := _.
+Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _.
 Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _.
-Proof. apply inr_inj'. Qed.
+Typeclasses Opaque sum_equiv.
 
 (** ** Option *)
 Instance option_inhabited {A} : Inhabited (option A) := populate None.

theories/option.v

@@ -122,7 +122,7 @@ Section setoids.
 
   Global Instance option_equivalence :
     Equivalence (≡@{A}) → Equivalence (≡@{option A}).
-  Proof. apply option_Forall2_equiv. Qed.
+  Proof. apply _. Qed.
   Global Instance Some_proper : Proper ((≡) ==> (≡@{option A})) Some.
   Proof. by constructor. Qed.
   Global Instance Some_equiv_inj : Inj (≡) (≡@{option A}) Some.

theories/streams.v

@@ -40,9 +40,9 @@ Lemma scons_equiv s1 s2 : shead s1 = shead s2 → stail s1 ≡ stail s2 → s1
 Proof. by constructor. Qed.
 Global Instance equal_equivalence : Equivalence (≡@{stream A}).
 Proof.
-  unfold equiv, stream_equiv. split.
-  - cofix FIX; intros [??]; by constructor.
-  - cofix FIX; intros ?? [??]; by constructor.
+  split.
+  - now cofix FIX; intros [??]; constructor.
+  - now cofix FIX; intros ?? [??]; constructor.
   - cofix FIX; intros ??? [??] [??]; constructor; etrans; eauto.
 Qed.
 Global Instance scons_proper x : Proper ((≡) ==> (≡)) (scons x).