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

make inv_heap_inv typeclass-opaque

parent cdaf17ee
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/base_logic/lib/gen_inv_heap.v
+ 7
− 4
View file @ 7f297859
...@@ -177,14 +177,17 @@ Section inv_heap. ...@@ -177,14 +177,17 @@ Section inv_heap.
apply: singletonM_proper. f_equiv. by apply: to_agree_proper. apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
Qed. Qed.
Global Instance inv_heap_inv_persistent : Persistent (inv_heap_inv L V).
Proof. apply _. Qed.
Global Instance inv_mapsto_persistent l I : Persistent (l ↦□ I). Global Instance inv_mapsto_persistent l I : Persistent (l ↦□ I).
Proof. rewrite /inv_mapsto. apply _. Qed. Proof. apply _. Qed.
Global Instance inv_mapsto_timeless l I : Timeless (l ↦□ I). Global Instance inv_mapsto_timeless l I : Timeless (l ↦□ I).
Proof. rewrite /inv_mapsto. apply _. Qed. Proof. apply _. Qed.
Global Instance inv_mapsto_own_timeless l v I : Timeless (l ↦_I v). Global Instance inv_mapsto_own_timeless l v I : Timeless (l ↦_I v).
Proof. rewrite /inv_mapsto. apply _. Qed. Proof. apply _. Qed.
(** * Public lemmas *) (** * Public lemmas *)
...@@ -281,4 +284,4 @@ Section inv_heap. ...@@ -281,4 +284,4 @@ Section inv_heap.
End inv_heap. End inv_heap.
Typeclasses Opaque inv_mapsto inv_mapsto_own. Typeclasses Opaque inv_heap_inv inv_mapsto inv_mapsto_own.
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