From cb563064db46beee2102087acc420202e954950b Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Mon, 22 Jan 2024 18:35:57 +0100
Subject: [PATCH] WIP multi_channel

---
 _CoqProject                    | 3 ++-
 theories/channel/multi_proto.v | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/_CoqProject b/_CoqProject
index 330aec8..2fcbc7e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -16,9 +16,10 @@ theories/utils/cofe_solver_2.v
 theories/utils/switch.v
 theories/channel/proto_model.v
 theories/channel/proto.v
+theories/channel/channel.v
 theories/channel/multi_proto_model.v
 theories/channel/multi_proto.v
-theories/channel/channel.v
+theories/channel/multi_channel.v
 theories/channel/proofmode.v
 theories/examples/basics.v
 theories/examples/equivalence.v
diff --git a/theories/channel/multi_proto.v b/theories/channel/multi_proto.v
index 984b84c..05b31f7 100644
--- a/theories/channel/multi_proto.v
+++ b/theories/channel/multi_proto.v
@@ -707,7 +707,7 @@ Section proto.
     iProto_own γ i (<(Send j)> m1) -∗
     iProto_own γ j (<(Recv i)> m2) -∗
     iMsg_car m1 v (Next p1) ==∗
-    ▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ ▷ iProto_ctx γ ∗
+    ▷ ∃ p2, iMsg_car m2 v (Next p2) ∗ iProto_ctx γ ∗
             iProto_own γ i p1 ∗ iProto_own γ j p2.
   Proof.
     iIntros "Hctx Hi Hj Hm".
@@ -718,7 +718,7 @@ Section proto.
       (p2) "[Hm2 Hconsistent]".
     iMod (iProto_own_auth_update _ _ _ _ p2 with "Hauth Hj") as "[Hauth Hj]".
     iMod (iProto_own_auth_update _ _ _ _ p1 with "Hauth Hi") as "[Hauth Hi]".
-    iIntros "!>!>". iExists p2. iFrame. iIntros "!>". iExists _. iFrame.
+    iIntros "!>!>". iExists p2. iFrame. iExists _. iFrame.
   Qed.
 
   (* (** The instances below make it possible to use the tactics [iIntros], *)
-- 
GitLab