From 7ec1d14ac036a72be002d95f4dcbf64a38e7b1a3 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Fri, 9 Sep 2016 14:39:33 +0200
Subject: [PATCH] Use non-primitive VS that take a step.
---
types.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/types.v b/types.v
index 875b82d7..c0d943c4 100644
--- a/types.v
+++ b/types.v
@@ -132,7 +132,7 @@ Section types.
★ ▷ l ↦★: ty.(ty_own) tid)%I;
ty_shr κ tid N l :=
(∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ★
- ∀ q', □ ([κ]{q'} →|={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ tid N l' ★ [κ]{q'}))%I
+ ∀ q', [κ]{q'} ={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ tid N l' ★ [κ]{q'})%I
|}.
Next Obligation.
iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
@@ -183,8 +183,8 @@ Section types.
(∃ l:loc, vl = [ #l ] ★ &{κ} l ↦★: ty.(ty_own) tid)%I;
ty_shr κ' tid N l :=
(∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ★
- ∀ q' κ'', □ (κ'' ⊑ κ ★ κ'' ⊑ κ' ★ [κ'']{q'} →
- |={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ'' tid N l' ★ [κ'']{q'}))%I
+ ∀ q' κ'', κ'' ⊑ κ ★ κ'' ⊑ κ' ★ [κ'']{q'}
+ ={mgmtE ∪ N, mgmtE}▷=> ty.(ty_shr) κ'' tid N l' ★ [κ'']{q'})%I
|}.
Next Obligation.
iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
--
GitLab