From a2f6e6a8e58aa9718b7fb779d0182cf4514de21f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 May 2020 14:57:36 +0200
Subject: [PATCH] More comment tweaking.

---
 theories/channel/channel.v |  8 ++++----
 theories/channel/proto.v   | 23 +++++++++++------------
 2 files changed, 15 insertions(+), 16 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 9ed9b22..d9c728f 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -6,9 +6,9 @@ lock-protected buffers, and their primitive proof rules. Moreover:
 - It proves Actris's specifications of [send] and [recv] w.r.t. dependent
   separation protocols.
 
-An encoding of the usual choice connectives [prot1 <{Q1}+{Q2}> prot2] and
-[prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in this
-file.
+An encoding of the usual (binary) choice connectives [prot1 <{Q1}+{Q2}> prot2]
+and [prot1 <{Q1}&{Q2}> prot2], inspired by session types, is also included in
+this file.
 
 In this file we define the three message-passing connectives:
 
@@ -46,7 +46,7 @@ Definition send : val :=
     acquire "lk";;
     let: "l" := Fst (Fst "c") in
     lsnoc "l" "v";;
-    skipN (llength (Snd (Fst "c")));; (* Later stripping *)
+    skipN (llength (Snd (Fst "c")));; (* "Ghost" operation for later stripping *)
     release "lk".
 
 Definition try_recv : val :=
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index f483fa0..bd8aa24 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -7,25 +7,24 @@ parameterized version in [proto_model] with the type of propositions [iProp] of
 We define ways of constructing instances of the instantiated type via two
 constructors:
 - [iProto_end], which is identical to [proto_end].
-- [iProto_message], which takes an [action] and an [iMsg] which is a
-  sequence of binders [iMsg_exist] terminated by the payload
-  constructed with [iMsg_base] based on arguments v, P and prot
-  which are the value, the carried proposition and the [iProto] tail
-  respectively.
+- [iProto_message], which takes an [action] and an [iMsg]. The type [iMsg] is a
+  sequence of binders [iMsg_exist], terminated by the payload constructed with
+  [iMsg_base] based on arguments [v], [P] and [prot], which are the value, the
+  carried proposition and the [iProto] tail, respectively.
 
 For convenience sake, we provide the following notations:
 - [END], which is simply [iProto_end].
-- [∃ x,m] which is [iMsg_exist] with argument m.
-- [MSG v ; {{ P }}; prot] which is [iMsg_Base with
-- [<a> m] which is [iProto_message] with arguments a and m.
+- [∃ x, m], which is [iMsg_exist] with argument [m].
+- [MSG v {{ P }}; prot], which is [iMsg_Base] with arguments [v], [P] and [prot].
+- [<a> m], which is [iProto_message] with arguments [a] and [m].
 
 We also include custom notation to more easily construct complete constructions:
-- [<a x1 .. xn> m] which is [<a> ∃ x1, .. ∃ xn, m]
-- [<a x1 .. xn> MSG v; {{ P }}; prot], which constructs a full protocol
+- [<a x1 .. xn> m], which is [<a> ∃ x1, .. ∃ xn, m].
+- [<a x1 .. xn> MSG v; {{ P }}; prot], which constructs a full protocol.
 
 Futhermore, we define the following operations:
-- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa
-- [iProto_app], which appends two protocols as described in proto_model.v
+- [iProto_dual], which turns all [Send] of a protocol into [Recv] and vice-versa.
+- [iProto_app], which appends two protocols.
 
 In addition we define the subprotocol relation [iProto_le] [⊑], which generalises
 the following inductive definition for asynchronous subtyping on session types:
-- 
GitLab