diff --git a/theories/mapset.v b/theories/mapset.v
index 72482ace2466ebe3e37a8049e7a88061cd55c83f..7481faadb0cd883f9d560dbad8ccd633de1b34fb 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -76,7 +76,7 @@ Section deciders.
     match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
     abstract congruence.
   Defined.
-  Program Instance mapset_countable `{Countable (M ())} : Countable (mapset M) :=
+  Global Program Instance mapset_countable `{Countable (M ())} : Countable (mapset M) :=
     inj_countable mapset_car (Some ∘ Mapset) _.
   Next Obligation. by intros ? ? []. Qed.
   Global Instance mapset_equiv_dec : RelDecision (≡@{mapset M}) | 1.