From 7f297859f3c2d12e20d281b648afd25bede87958 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 18 Apr 2020 22:06:09 +0200
Subject: [PATCH] make inv_heap_inv typeclass-opaque
---
theories/base_logic/lib/gen_inv_heap.v | 11 +++++++----
1 file changed, 7 insertions(+), 4 deletions(-)
diff --git a/theories/base_logic/lib/gen_inv_heap.v b/theories/base_logic/lib/gen_inv_heap.v
index 79a0736aa..0031b43bd 100644
--- a/theories/base_logic/lib/gen_inv_heap.v
+++ b/theories/base_logic/lib/gen_inv_heap.v
@@ -177,14 +177,17 @@ Section inv_heap.
apply: singletonM_proper. f_equiv. by apply: to_agree_proper.
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).
- Proof. rewrite /inv_mapsto. apply _. Qed.
+ Proof. apply _. Qed.
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).
- Proof. rewrite /inv_mapsto. apply _. Qed.
+ Proof. apply _. Qed.
(** * Public lemmas *)
@@ -281,4 +284,4 @@ Section inv_heap.
End inv_heap.
-Typeclasses Opaque inv_mapsto inv_mapsto_own.
+Typeclasses Opaque inv_heap_inv inv_mapsto inv_mapsto_own.
--
GitLab