Commit 947d9147 authored by Ralf Jung's avatar Ralf Jung
Browse files

remove Dom instances with alternative domain types

parent b7a5fed7
......@@ -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.
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment