From 91391d2e582ca3d54dadf591a0a7ebbbee1ee3a1 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 20 Jul 2020 17:44:45 +0200
Subject: [PATCH] Removed redundant later

---
 theories/channel/channel.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index e02f321..d80dec8 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -235,9 +235,9 @@ Section channel.
   Qed.
 
   Lemma try_recv_spec {TT} c (v : TT → val) (P : TT → iProp Σ) (p : TT → iProto Σ) :
-    {{{ c ↣ <?.. x> MSG v x {{ ▷ P x }}; p x }}}
+    {{{ c ↣ <?.. x> MSG v x {{ P x }}; p x }}}
       try_recv c
-    {{{ w, RET w; (⌜w = NONEV⌝ ∗ c ↣ <?.. x> MSG v x {{ ▷ P x }}; p x) ∨
+    {{{ w, RET w; (⌜w = NONEV⌝ ∗ c ↣ <?.. x> MSG v x {{ P x }}; p x) ∨
                   (∃.. x, ⌜w = SOMEV (v x)⌝ ∗ c ↣ p x ∗ P x) }}}.
   Proof.
     assert (∀ w lp (m : TT → iMsg Σ),
-- 
GitLab