summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Values.ml7
1 files changed, 5 insertions, 2 deletions
diff --git a/src/Values.ml b/src/Values.ml
index 8ecf8849..a0bd96c5 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -54,10 +54,13 @@ type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty }
- a projector on loans may see a symbolic value of id `sid` as having type `T`
- a projector on borrows may see it as having type `&mut T`
We need to make this clear and more consistant.
- So [symbolic_value] is actually a projector. TODO: rename
+ So [symbolic_value] is actually a projector. TODO: rename to [symbolic_proj].
+ The kind of projector will then depend on the context.
*)
-(** TODO: make it clear that complementary projectors are projectors on borrows *)
+(** TODO: make it clear that complementary projectors are projectors on borrows.
+ ** TODO: actually this is useless: the set of ended regions should be global!
+ ** (and thus stored in the context) *)
type symbolic_proj_comp = {
svalue : symbolic_value; (** The symbolic value itself *)
rset_ended : RegionId.set_t;