From db4dff939e9a041eb4f37a8469df8232dbbe4c69 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 17 Feb 2020 14:01:58 +0100
Subject: [PATCH] Remove more laters.
---
theories/channel/proto_channel.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index ea3b97e..013f028 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -248,8 +248,8 @@ Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ :=
chan_own (proto_c_name γ) Right r ∗
proto_own_auth γ Left pl ∗
proto_own_auth γ Right pr ∗
- ▷ ((⌜r = []⌠∗ proto_interp l pl pr) ∨
- (⌜l = []⌠∗ proto_interp r pr pl)))%I.
+ ((⌜r = []⌠∗ proto_interp l pl pr) ∨
+ (⌜l = []⌠∗ proto_interp r pr pl)))%I.
Definition protoN := nroot .@ "proto".
@@ -728,7 +728,7 @@ Section proto.
iFrame "Hcctx Hinv Hst". iSplit; first done.
rewrite iProto_le_unfold. iRight; auto 10.
+ iIntros (v vs ->) "Hcr".
- iDestruct "Hinv'" as "[[>% _]|[>-> Heval]]"; first done.
+ iDestruct "Hinv'" as "[[% _]|[-> Heval]]"; first done.
iAssert (â–· proto_interp (v :: vs) pr (proto_message Receive pc'))%I
with "[Heval]" as "Heval".
{ iNext. by iRewrite "Heq" in "Heval". }
@@ -751,7 +751,7 @@ Section proto.
iFrame "Hcctx Hinv Hst". iSplit; first done.
rewrite iProto_le_unfold. iRight; auto 10.
+ iIntros (v vs ->) "Hcl".
- iDestruct "Hinv'" as "[[>-> Heval]|[>% _]]"; last done.
+ iDestruct "Hinv'" as "[[-> Heval]|[% _]]"; last done.
iAssert (â–· proto_interp (v :: vs) pl (proto_message Receive pc'))%I
with "[Heval]" as "Heval".
{ iNext. by iRewrite "Heq" in "Heval". }
--
GitLab