From 2c93d514d6d62f8eccba47b1efefa2db1e56954e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 19 Jan 2022 01:24:35 +0100
Subject: Implement the sanity checks for consumption of symbolic values by
 abstractions (as input or given back values)

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

(limited to 'src/Values.ml')

diff --git a/src/Values.ml b/src/Values.ml
index a64d4467..6386f8db 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -232,6 +232,10 @@ type aproj =
       (** When ending a proj_loans over a symbolic value, we may need to insert
           (and keep track of) a proj_borrows over the given back value, if the
           symbolic value was consumed by an abstraction then updated.
+          
+          Rk.: for now this is useless, because we forbid borrow overwrites on
+          returned values. A consequence is that when a proj_loans over a symbolic
+          value ends, we don't project the given back value.
        *)
   | AEndedProjBorrows
   (* TODO: remove AEndedProjBorrows? We might need it for synthesis, to contain
-- 
cgit v1.2.3