From 12272f3e3f87fbe6c3b7091cd83411a346319761 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 13 Apr 2017 14:29:54 +0200
Subject: [PATCH] use lock_proto only under a later

---
 theories/lang/lib/lock.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 001dbfb5..121a2ac5 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -46,7 +46,7 @@ Section proof.
 
   (** The main proofs. *)
   Lemma lock_proto_create (E : coPset) (R : iProp Σ) l (b : bool) :
-    l ↦ #b -∗ (if b then True else R) ={E}=∗ ∃ γ, lock_proto γ l R.
+    l ↦ #b -∗ (if b then True else ▷ R) ={E}=∗ ∃ γ, ▷ lock_proto γ l R.
   Proof.
     iIntros "Hl HR".
     iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
@@ -55,9 +55,9 @@ Section proof.
 
   Lemma lock_proto_destroy E γ l R :
     ↑N ⊆ E → 
-    lock_proto γ l R ={E}=∗ ∃ (b : bool), l ↦ #b ∗ if b then True else R.
+    ▷ lock_proto γ l R ={E}=∗ ∃ (b : bool), l ↦ #b ∗ if b then True else ▷ R.
   Proof.
-    iIntros (?) "Hlck". iDestruct "Hlck" as (b) "[Hl HR]".
+    iIntros (?) "Hlck". iDestruct "Hlck" as (b) "[>Hl HR]".
     iExists b. iFrame "Hl". destruct b; first done.
     iDestruct "HR" as "[_ $]". done.
   Qed.
@@ -65,9 +65,9 @@ Section proof.
   (* At this point, it'd be really nice to have some sugar for symmetric
      accessors. *)
   Lemma try_acquire_spec E γ l R P :
-    □ (P ={E,∅}=∗ lock_proto γ l R ∗ (lock_proto γ l R ={∅,E}=∗ P)) -∗
+    □ (P ={E,∅}=∗ ▷ lock_proto γ l R ∗ (▷ lock_proto γ l R ={∅,E}=∗ P)) -∗
     {{{ P }}} try_acquire [ #l ] @ E
-    {{{ b, RET #b; (if b is true then locked γ ∗ R else True) ∗ P }}}.
+    {{{ b, RET #b; (if b is true then locked γ ∗ ▷ R else True) ∗ P }}}.
   Proof.
     iIntros "#Hproto !# * HP HΦ".
     wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
@@ -82,8 +82,8 @@ Section proof.
   Qed.
 
   Lemma acquire_spec E γ l R P :
-    □ (P ={E,∅}=∗ lock_proto γ l R ∗ (lock_proto γ l R ={∅,E}=∗ P)) -∗
-    {{{ P }}} acquire [ #l ] @ E {{{ RET #(); locked γ ∗ R ∗ P }}}.
+    □ (P ={E,∅}=∗ ▷ lock_proto γ l R ∗ (▷ lock_proto γ l R ={∅,E}=∗ P)) -∗
+    {{{ P }}} acquire [ #l ] @ E {{{ RET #(); locked γ ∗ ▷ R ∗ P }}}.
   Proof.
     iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
     iPoseProof (try_acquire_spec with "[Hproto] * HP") as "Hacq".
@@ -96,7 +96,7 @@ Section proof.
   Qed.
 
   Lemma release_spec E γ l R P :
-    □ (P ={E,∅}=∗ lock_proto γ l R ∗ (lock_proto γ l R ={∅,E}=∗ P)) -∗
+    □ (P ={E,∅}=∗ ▷ lock_proto γ l R ∗ (▷ lock_proto γ l R ={∅,E}=∗ P)) -∗
     {{{ locked γ ∗ R ∗ P }}} release [ #l ] @ E {{{ RET #(); P }}}.
   Proof.
     iIntros "#Hproto !# * (Hlocked & HR & HP) HΦ". wp_let.
-- 
GitLab