diff --git a/theories/coGset.v b/theories/coGset.v
index 4a0f75e2c1b98ad2b81645a8198df78e0cdecdba..57590d44c03fbf4206fbf3c5a582a6bf7a099ed6 100644
--- a/theories/coGset.v
+++ b/theories/coGset.v
@@ -192,15 +192,5 @@ Lemma elem_of_coGset_to_top_set `{Countable A, TopSet A C} X x :
   x ∈@{C} coGset_to_top_set X ↔ x ∈ X.
 Proof. destruct X; set_solver. Qed.
 
-(** * Domain of finite maps *)
-Global Instance coGset_dom `{Countable K} {A} : Dom (gmap K A) (coGset K) := λ m,
-  gset_to_coGset (dom _ m).
-Global Instance coGset_dom_spec `{Countable K} : FinMapDom K (gmap K) (coGset K).
-Proof.
-  split; try apply _. intros B m i. unfold dom, coGset_dom.
-  by rewrite elem_of_gset_to_coGset, elem_of_dom.
-Qed.
-
 Typeclasses Opaque coGset_elem_of coGset_empty coGset_top coGset_singleton.
 Typeclasses Opaque coGset_union coGset_intersection coGset_difference.
-Typeclasses Opaque coGset_dom.
diff --git a/theories/coPset.v b/theories/coPset.v
index 8e8cb978c846d563b3c6c2042efe6805cecea937..1e2c3765f63001fac745492104bf7ea9a735d258 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -358,21 +358,6 @@ Proof.
   refine (cast_if (decide (¬set_finite X))); by rewrite coPset_infinite_finite.
 Defined.
 
-(** * Domain of finite maps *)
-Global Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, Pset_to_coPset (dom _ m).
-Global Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
-Proof.
-  split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
-  by rewrite elem_of_Pset_to_coPset, elem_of_dom.
-Qed.
-Global Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
-  gset_to_coPset (dom _ m).
-Global Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
-Proof.
-  split; try apply _; intros A m i; unfold dom, gmap_dom_coPset.
-  by rewrite elem_of_gset_to_coPset, elem_of_dom.
-Qed.
-
 (** * Suffix sets *)
 Fixpoint coPset_suffixes_raw (p : positive) : coPset_raw :=
   match p with