Skip to content
Snippets Groups Projects
Commit e0eef94a authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix compilation after !112 broke it.

parent f84c69f6
No related branches found
No related tags found
No related merge requests found
......@@ -159,8 +159,6 @@ Instance coPset_singleton : Singleton positive coPset := λ p,
Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
Instance coPset_empty : Empty coPset := coPLeaf false I.
Instance coPset_top : Top coPset := coPLeaf true I.
(** Iris and specifically [solve_ndisj] heavily rely on this hint. *)
Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : core.
Instance coPset_union : Union coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 t2) coPset_union_wf _ _ Ht1 Ht2.
......@@ -186,6 +184,9 @@ Proof.
- done.
Qed.
(** Iris and specifically [solve_ndisj] heavily rely on this hint. *)
Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : core.
Instance coPset_leibniz : LeibnizEquiv coPset.
Proof.
intros X Y; rewrite elem_of_equiv; intros HXY.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment