From 4f7244115b294ff4724a95a2eb97971fc50a6468 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Mon, 20 Nov 2023 15:54:34 +0100
Subject: [PATCH] Bumped Iris

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

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 448cffe..f1f8584 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -206,9 +206,7 @@ Section channel.
       new_chan #()
     {{{ c1 c2, RET (c1,c2); c1 ↣ p ∗ c2 ↣ iProto_dual p }}}.
   Proof.
-    iIntros (Φ _) "HΦ". wp_lam.
-    wp_bind (lnil _).
-    iApply wp_lb_init; iIntros "#Hlb".
+    iIntros (Φ _) "HΦ". wp_lam. iMod (steps_lb_0) as "#Hlb".
     wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (l) "Hl".
     wp_smart_apply (lnil_spec internal_eq with "[//]"); iIntros (r) "Hr".
     iMod (iProto_init p) as (γp) "(Hctx & Hcl & Hcr)".
-- 
GitLab