diff options
| author | Son Ho | 2022-12-02 01:22:02 +0100 |
|---|---|---|
| committer | Son HO | 2023-02-03 11:21:46 +0100 |
| commit | b2a494f8fc3acdf1cfab7b4d6d10b1bd316663f8 (patch) | |
| tree | bbb14e02331c639173bc64d6e84246a918bf3ab4 | |
| parent | f001e68a591750c9e7265cb331fd42cfadefa05d (diff) | |
Update a comment
| -rw-r--r-- | compiler/Values.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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. |