From d0961b678540fda6d4749a7f40d5a279beddffbc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 14 Mar 2019 10:30:05 +0100
Subject: [PATCH] Make `mapset_countable` a global instance.

---
 theories/mapset.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/mapset.v b/theories/mapset.v
index 72482ace..7481faad 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.
-- 
GitLab