From 777d9fe1c25a2bed3191d71950a1b0b2e62c29c7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 17 Feb 2020 13:37:33 +0100
Subject: [PATCH] Remove more useless laters.
---
theories/channel/proto_channel.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index 1a69f5d..ea3b97e 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -597,9 +597,9 @@ Section proto.
Qed.
Lemma proto_interp_recv v vs p1 pc :
- proto_interp (v :: vs) p1 (proto_message Receive pc) -∗ ∃ p2,
- pc v (proto_eq_next p2) ∗
- â–· proto_interp vs p1 p2.
+ proto_interp (v :: vs) p1 (proto_message Receive pc) -∗ ∃ p2,
+ pc v (proto_eq_next p2) ∗
+ proto_interp vs p1 p2.
Proof.
simpl. iDestruct 1 as (pc' p2) "(Heq & Hc & Hp2)". iExists p2. iFrame "Hp2".
iDestruct (@proto_message_equivI with "Heq") as "[_ Heq]".
--
GitLab