diff --git a/algebra/cmra.v b/algebra/cmra.v
index e01c27716452285a0ff22ec31210cda3a8275a50..167f75c5e90064b130f307a0fd329356cb9e6e2e 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -76,7 +76,10 @@ Arguments cmra_validN : simpl never.
 Arguments cmra_cofe_mixin : simpl never.
 Arguments cmra_mixin : simpl never.
 Add Printing Constructor cmraT.
-Existing Instances cmra_pcore cmra_op cmra_valid cmra_validN.
+Hint Extern 0 (PCore _) => eapply (@cmra_pcore _) : typeclass_instances.
+Hint Extern 0 (Op _) => eapply (@cmra_op _) : typeclass_instances.
+Hint Extern 0 (Valid _) => eapply (@cmra_valid _) : typeclass_instances.
+Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
 Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A (cmra_cofe_mixin A).
 Canonical Structure cmra_cofeC.
 
@@ -174,7 +177,7 @@ Arguments ucmra_cofe_mixin : simpl never.
 Arguments ucmra_cmra_mixin : simpl never.
 Arguments ucmra_mixin : simpl never.
 Add Printing Constructor ucmraT.
-Existing Instances ucmra_empty.
+Hint Extern 0 (Empty _) => eapply (@ucmra_empty _) : typeclass_instances.
 Coercion ucmra_cofeC (A : ucmraT) : cofeT := CofeT A (ucmra_cofe_mixin A).
 Canonical Structure ucmra_cofeC.
 Coercion ucmra_cmraR (A : ucmraT) : cmraT :=
diff --git a/algebra/cofe.v b/algebra/cofe.v
index dcfaa63558459411457966b8a864ed7f2640dee6..f628b2fe9201dd429fd653d261101f437e5f1535 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -67,7 +67,9 @@ Structure cofeT := CofeT {
 }.
 Arguments CofeT _ {_ _ _} _.
 Add Printing Constructor cofeT.
-Existing Instances cofe_equiv cofe_dist cofe_compl.
+Hint Extern 0 (Equiv _) => eapply (@cofe_equiv _) : typeclass_instances.
+Hint Extern 0 (Dist _) => eapply (@cofe_dist _) : typeclass_instances.
+Hint Extern 0 (Compl _) => eapply (@cofe_compl _) : typeclass_instances.
 Arguments cofe_car : simpl never.
 Arguments cofe_equiv : simpl never.
 Arguments cofe_dist : simpl never.