From b2a494f8fc3acdf1cfab7b4d6d10b1bd316663f8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 2 Dec 2022 01:22:02 +0100
Subject: Update a comment

---
 compiler/Values.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/Values.ml b/compiler/Values.ml
index 7f6808ae..54575edd 100644
--- a/compiler/Values.ml
+++ b/compiler/Values.ml
@@ -665,7 +665,10 @@ and aborrow_content =
           Rem.: we don't use the meta-value for now, but might need it when
           using nested borrows: if we end an *internal* borrow, this meta
           value is propagated to the corresponding loan (we need to know
-          what the loan consumed, for the synthesis).
+          what the loan consumed, for the synthesis). We could also generate
+          a fresh symbolic value upon ending the internal borrow (as is
+          done in the regular case), which would allow us to remove the
+          meta-value altogether.
      *)
   | ASharedBorrow of borrow_id
       (** A shared borrow owned by an abstraction.
-- 
cgit v1.2.3