From c8bcb18d6e29c1ad9efa8f178e7699d1a94db96c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 3 Aug 2017 20:54:31 +0200
Subject: [PATCH] These are spurious laters.
---
theories/lang/lib/lock.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 446804dd..3832cceb 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -73,7 +73,7 @@ Section proof.
Lemma try_acquire_spec E l R 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 ▷ R else True) ∗ P }}}.
+ {{{ b, RET #b; (if b is true then R else True) ∗ P }}}.
Proof.
iIntros "#Hproto !# * HP HΦ".
wp_rec. iMod ("Hproto" with "HP") as "(Hinv & Hclose)".
@@ -88,7 +88,7 @@ Section proof.
Lemma acquire_spec E l R P :
□ (P ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ P)) -∗
- {{{ P }}} acquire [ #l ] @ E {{{ RET #(); ▷ R ∗ P }}}.
+ {{{ P }}} acquire [ #l ] @ E {{{ RET #(); R ∗ P }}}.
Proof.
iIntros "#Hproto !# * HP HΦ". iLöb as "IH". wp_rec.
wp_apply (try_acquire_spec with "Hproto HP"). iIntros ([]).
--
GitLab