diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Values.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Values.ml b/src/Values.ml index 3314defb..3f1fc0bd 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -144,7 +144,7 @@ and borrow_content = *) | MutBorrow of (BorrowId.id[@opaque]) * typed_value (** A mutably borrowed value. *) - | InactivatedMutBorrow of (BorrowId.id[@opaque]) + | InactivatedMutBorrow of mvalue * (BorrowId.id[@opaque]) (** An inactivated mut borrow. This is used to model [two-phase borrows](https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html). @@ -169,6 +169,10 @@ and borrow_content = l = Vec::len(move v2); Vec::push(move v1, move l); // In practice, v1 gets activated only here ``` + + The meta-value is used for the same purposes as with shared borrows, + at the exception that in case of inactivated borrows it is not + *necessary* for the synthesis: we keep it only as meta-information. *) and loan_content = |