summaryrefslogtreecommitdiff
path: root/src/Values.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/Values.ml')
-rw-r--r--src/Values.ml8
1 files changed, 8 insertions, 0 deletions
diff --git a/src/Values.ml b/src/Values.ml
index c9dff56a..53851cea 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -473,6 +473,14 @@ and aborrow_content =
> }
```
+
+ Note that we could use AIgnoredMutLoan in the case the borrow id is not
+ None, which would allow us to simplify the rules (to not have rules
+ to specifically handle the case of AIgnoredMutBorrow with Some borrow
+ id) and also remove the AEndedIgnoredMutBorrow variant.
+ For now, the rules are implemented and it allows us to make the avalues
+ more precise and clearer, so we will keep it that way.
+
TODO: this is annoying, we are duplicating information. Maybe we
could introduce an "Ignored" value? We have to pay attention to
two things: