diff --git a/theories/Programming/Eqv.v b/theories/Programming/Eqv.v
index 8bcd804..72d710d 100644
--- a/theories/Programming/Eqv.v
+++ b/theories/Programming/Eqv.v
@@ -6,9 +6,11 @@ Class Eqv T := eqv : T -> T -> Prop.
 Definition neg_eqv {T} {E:Eqv T} (x:T) (y:T) : Prop := not (eqv x y).
 
 Class EqvWF T :=
-{ eqvWFEqv :> Eqv T
-; eqvWFEquivalence :> Equivalence eqv
+{ eqvWFEqv : Eqv T
+; eqvWFEquivalence : Equivalence eqv
 }.
+#[global] Existing Instance eqvWFEqv.
+#[global] Existing Instance eqvWFEquivalence.
 #[global]
 Instance EqvWF_Build {T} {E:Eqv T} {EV:Equivalence eqv} : EqvWF T :=
   { eqvWFEqv := E ; eqvWFEquivalence := EV }.
diff --git a/theories/Programming/Le.v b/theories/Programming/Le.v
index 017fe04..2b4d019 100644
--- a/theories/Programming/Le.v
+++ b/theories/Programming/Le.v
@@ -27,9 +27,11 @@ Proof. constructor.
 Qed.
 
 Class LteWF T :=
-{ lteWFLte :> Lte T
-; lteWFPreOrder :> PreOrder lte
+{ lteWFLte : Lte T
+; lteWFPreOrder : PreOrder lte
 }.
+#[global] Existing Instance lteWFLte.
+#[global] Existing Instance lteWFPreOrder.
 
 #[global]
 Instance LteWF_Build {T} {L:Lte T} {PO:PreOrder lte} : LteWF T :=
diff --git a/theories/Structures/Monoid.v b/theories/Structures/Monoid.v
index ad73f08..b9d574b 100644
--- a/theories/Structures/Monoid.v
+++ b/theories/Structures/Monoid.v
@@ -14,9 +14,12 @@ Section Monoid.
   }.
 
   Class MonoidLaws@{} (M : Monoid) : Type :=
-  { monoid_assoc :> Associative M.(monoid_plus) eq
-  ; monoid_lunit :> LeftUnit M.(monoid_plus) M.(monoid_unit) eq
-  ; monoid_runit :> RightUnit M.(monoid_plus) M.(monoid_unit) eq
+  { monoid_assoc : Associative M.(monoid_plus) eq
+  ; monoid_lunit : LeftUnit M.(monoid_plus) M.(monoid_unit) eq
+  ; monoid_runit : RightUnit M.(monoid_plus) M.(monoid_unit) eq
   }.
+  #[global] Existing Instance monoid_assoc.
+  #[global] Existing Instance monoid_lunit.
+  #[global] Existing Instance monoid_runit.
 
 End Monoid.