Library MathClasses.misc.workarounds

Require Import MathClasses.interfaces.canonical_names.
Require Import Coq.Classes.Equivalence Coq.Classes.Morphisms Coq.Classes.RelationClasses.

Remove Hints Equivalence_Reflexive
  equiv_reflexive
  Equivalence_Symmetric
  equiv_symmetric
  Equivalence_Transitive
  equiv_transitive : typeclass_instances.

Hint Extern 0 (Reflexive _) => apply @Equivalence_Reflexive : typeclass_instances.
Hint Extern 0 (Symmetric _) => apply @Equivalence_Symmetric : typeclass_instances.
Hint Extern 0 (Transitive _) => apply @Equivalence_Transitive : typeclass_instances.


Instance equivalence_proper `{Equivalence A R} : Proper (R ==> R ==> iff) R | 0 := _.