From 773c0bb9d94bdcad2ecdc95ce4cbdf1ee4f1b89d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 11 Nov 2017 11:17:05 +0100
Subject: [PATCH] saved_proper: also provide strong allocation

---
 theories/base_logic/lib/saved_prop.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index d81ec9c98..c4053dab2 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -62,6 +62,10 @@ Notation savedPropΣ := (savedAnythingΣ (▶ ∙)).
 Definition saved_prop_own `{savedPropG Σ} (γ : gname) (P: iProp Σ) :=
   saved_anything_own (F := ▶ ∙) γ (Next P).
 
+Lemma saved_prop_alloc_strong `{savedPropG Σ} (G : gset gname) (P: iProp Σ) :
+  (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_prop_own γ P)%I.
+Proof. iApply saved_anything_alloc_strong. Qed.
+
 Lemma saved_prop_alloc `{savedPropG Σ} (P: iProp Σ) :
   (|==> ∃ γ, saved_prop_own γ P)%I.
 Proof. iApply saved_anything_alloc. Qed.
@@ -79,6 +83,10 @@ Notation savedPredΣ A := (savedAnythingΣ (constCF A -n> ▶ ∙)).
 Definition saved_pred_own `{savedPredG Σ A} (γ : gname) (f: A -n> iProp Σ) :=
   saved_anything_own (F := A -n> ▶ ∙) γ (CofeMor Next ◎ f).
 
+Lemma saved_pred_alloc_strong `{savedPredG Σ A} (G : gset gname) (f: A -n> iProp Σ) :
+  (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ saved_pred_own γ f)%I.
+Proof. iApply saved_anything_alloc_strong. Qed.
+
 Lemma saved_pred_alloc `{savedPredG Σ A} (f: A -n> iProp Σ) :
   (|==> ∃ γ, saved_pred_own γ f)%I.
 Proof. iApply saved_anything_alloc. Qed.
-- 
GitLab