From 947d91476f41bb96b3335c1627ea995a58f74e01 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 7 May 2022 11:03:49 +0200
Subject: [PATCH] remove Dom instances with alternative domain types

---
 theories/coGset.v | 10 ----------
 theories/coPset.v | 15 ---------------
 2 files changed, 25 deletions(-)

diff --git a/theories/coGset.v b/theories/coGset.v
index 4a0f75e2..57590d44 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 8e8cb978..1e2c3765 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
-- 
GitLab