diff options
Diffstat (limited to 'compiler')
| -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. |