Nits

theories/channel/channel.v

@@ -43,10 +43,11 @@ Definition start_chan : val := λ: "f",
 Definition send : val :=
   λ: "c" "v",
     let: "lk" := Snd "c" in
-    acquire "lk";;
     let: "l" := Fst (Fst "c") in
+    let: "r" := Snd (Fst "c") in
+    acquire "lk";;
     lsnoc "l" "v";;
-    skipN (llength (Snd (Fst "c")));; (* "Ghost" operation for later stripping *)
+    skipN (llength "r");; (* "Ghost" operation for later stripping *)
     release "lk".
 
 Definition try_recv : val :=

theories/channel/proto.v

@@ -708,6 +708,7 @@ Section proto.
     - iApply iProto_le_recv. iIntros (v' p') "(->&Hp&$) !>".
       iExists p2. iSplit; [|by auto]. iIntros "!>". by iRewrite -"Hp".
   Qed.
+
   Lemma iProto_le_base_swap v1 v2 P1 P2 p :
     ⊢ (<?> MSG v1 {{ P1 }}; <!> MSG v2 {{ P2 }}; p)
     ⊑ (<!> MSG v2 {{ P2 }}; <?> MSG v1 {{ P1 }}; p).
@@ -1297,6 +1298,7 @@ Section proto.
     FromModal (modality_instances.modality_laterN 1) (p1 ⊑ p2)
               ((<a> MSG v; p1) ⊑ (<a> MSG v; p2)) (p1 ⊑ p2).
   Proof. apply iProto_le_base. Qed.
+
 End proto.
 
 Typeclasses Opaque iProto_ctx iProto_own.

theories/examples/subprotocols.v

 From actris.channel Require Import proofmode proto channel.
-From actris.logrel Require Import subtyping_rules.
 From iris.proofmode Require Import tactics.
 From actris.utils Require Import llist.