From b33e4bfc7a32efc6ebbd385328e6350e0e5802bc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 20 Apr 2022 16:09:14 +0200
Subject: Add comments

---
 src/Values.ml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/Values.ml b/src/Values.ml
index d415df52..a3dfb84a 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -336,6 +336,9 @@ type aproj =
       (** The only purpose of [AEndedProjBorrows] is to store, for synthesis
           purposes, the symbolic value which was originally in the borrow projection,
           and the symbolic value which was generated and given back upon ending the borrow.
+       
+          The given back value is necessary for the synthesis. The orignal value is
+          useful to propagate naming constraints.
        *)
   | AIgnoredProjBorrows
 [@@deriving
@@ -682,6 +685,10 @@ and aborrow_content =
       (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value
           that we gave back as a meta-value, to help with the synthesis, together
           with the initial consumed value (also as a meta-value).
+
+          The given back value is necessary for the synthesis. The orignal consumed
+          value is useful to propagate naming constraints.
+
           We also remember the child [avalue] because this structural information
           is useful for the synthesis (but not for the symbolic execution):
           in practice the child value should only contain ended borrows, ignored
-- 
cgit v1.2.3