diff --git a/theories/gmap.v b/theories/gmap.v
index db96eba4ad9d941c2c2755c2e21cd39cadb37853..4f0b0dce033d4b3ebe7d05d28f8d8c7903f564d2 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -112,6 +112,16 @@ Proof.
     by rewrite lookup_merge by done; destruct (m1 !! _), (m2 !! _).
 Qed.
 
+Program Instance gmap_countable
+    `{Countable K, Countable A} : Countable (gmap K A) := {
+  encode m := encode (map_to_list m : list (K * A));
+  decode p := map_of_list <$> decode p
+}.
+Next Obligation.
+  intros K ?? A ?? m; simpl. rewrite decode_encode; simpl.
+  by rewrite map_of_to_list.
+Qed.
+
 (** * Finite sets *)
 Notation gset K := (mapset (gmap K)).
 Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
diff --git a/theories/pmap.v b/theories/pmap.v
index 6462ab0374edea4a81fc779ff12267fc4d871ade..8237bdccef4cbdedff419336230c5459817dd990 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -8,7 +8,7 @@ However, we extend Leroy's implementation by packing the trees into a Sigma
 type such that canonicity of representation is ensured. This is necesarry for
 Leibniz equality to become extensional. *)
 From Coq Require Import PArith.
-From stdpp Require Import mapset.
+From stdpp Require Import mapset countable.
 From stdpp Require Export fin_maps.
 
 Local Open Scope positive_scope.
@@ -300,11 +300,19 @@ Proof.
   - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
 Qed.
 
+Program Instance Pmap_countable `{Countable A} : Countable (Pmap A) := {
+  encode m := encode (map_to_list m : list (positive * A));
+  decode p := map_of_list <$> decode p
+}.
+Next Obligation.
+  intros A ?? m; simpl. rewrite decode_encode; simpl. by rewrite map_of_to_list.
+Qed.
+
 (** * Finite sets *)
 (** We construct sets of [positives]s satisfying extensional equality. *)
 Notation Pset := (mapset Pmap).
 Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
-Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
+Instance Pmap_dom_spec : FinMapDom positive Pmap Pset := mapset_dom_spec.
 
 (** * Fresh numbers *)
 Fixpoint Pdepth {A} (m : Pmap_raw A) : nat :=