diff options
| author | Son Ho | 2021-12-17 19:44:12 +0100 |
|---|---|---|
| committer | Son Ho | 2021-12-17 19:44:12 +0100 |
| commit | 71c7942870c8f6c849aef974f052f6037bbd44a7 (patch) | |
| tree | 8397b47a763b9cd2c060616f48bd2ae2329f169c | |
| parent | 8d9d0e5c038bf6e7e60be24d7289119210e8e67b (diff) | |
Add a comment
| -rw-r--r-- | src/Values.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/Values.ml b/src/Values.ml index c2def762..969e01d2 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -255,7 +255,8 @@ and aloan_content = | AIgnoredMutLoan of (BorrowId.id[@opaque]) * typed_avalue | AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue } | AProjSharedLoan of (abstract_shared_borrows[@opaque]) - (** A projected shared loan *) + (** A projected shared loan - TODO: remove? Does it make sense? Maybe + I should rename that to AIgnoredSharedLoan... *) (** Note that when a borrow content is ended, it is replaced by Bottom (while we need to track ended loans more precisely, especially because of their |