From ffc30e68c840d62abd152a2ecc4d086c4e9f148e Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 24 Jul 2020 15:44:31 +0200
Subject: [PATCH] Nits

---
 theories/channel/channel.v       | 5 +++--
 theories/channel/proto.v         | 2 ++
 theories/examples/subprotocols.v | 1 -
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index d80dec8..5b9f353 100644
--- a/theories/channel/channel.v
+++ b/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 :=
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 4190a72..f6b965f 100644
--- a/theories/channel/proto.v
+++ b/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.
diff --git a/theories/examples/subprotocols.v b/theories/examples/subprotocols.v
index b6dbab1..d828053 100644
--- a/theories/examples/subprotocols.v
+++ b/theories/examples/subprotocols.v
@@ -1,5 +1,4 @@
 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.
 
-- 
GitLab