Skip to content
Snippets Groups Projects
Commit 829dc991 authored by Ralf Jung's avatar Ralf Jung
Browse files

add comment

parent a5ee0c16
No related branches found
No related tags found
1 merge request!112move coPset-generic hint to coPset.v
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 0 deletions
theories/coPset.v
+ 1
− 0
View file @ 829dc991
...@@ -159,6 +159,7 @@ Instance coPset_singleton : Singleton positive coPset := λ p, ...@@ -159,6 +159,7 @@ Instance coPset_singleton : Singleton positive coPset := λ p,
Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X). Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
Instance coPset_empty : Empty coPset := coPLeaf false ↾ I. Instance coPset_empty : Empty coPset := coPLeaf false ↾ I.
Instance coPset_top : Top coPset := coPLeaf true ↾ 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. Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : core.
Instance coPset_union : Union coPset := λ X Y, Instance coPset_union : Union coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in let (t1,Ht1) := X in let (t2,Ht2) := Y in
......
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