diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 1878402b51a39919fa2f50574356441ad179cf51..773b72e0cef7be13d54631a708fee58dfcbd9864 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -7,14 +7,18 @@ Record gmultiset A `{Countable A} := GMultiSet { gmultiset_car : gmap A nat }.
 Arguments GMultiSet {_ _ _} _.
 Arguments gmultiset_car {_ _ _} _.
 
-Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
+Lemma gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
 Proof. solve_decision. Defined.
+Hint Extern 1 (Decision (@eq (gmultiset _) _ _)) =>
+  eapply @gmultiset_eq_dec : typeclass_instances.
 
-Program Instance gmultiset_countable `{Countable A} :
+Program Definition gmultiset_countable `{Countable A} :
     Countable (gmultiset A) := {|
   encode X := encode (gmultiset_car X);  decode p := GMultiSet <$> decode p
 |}.
 Next Obligation. intros A ?? [X]; simpl. by rewrite decode_encode. Qed.
+Hint Extern 1 (Countable (gmultiset _)) =>
+  eapply @gmultiset_countable : typeclass_instances.
 
 Section definitions.
   Context `{Countable A}.