summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-05 10:17:29 +0100
committerSon Ho2022-01-05 10:17:29 +0100
commitd658ff64adc746523568577668ce80034071d963 (patch)
tree6e8e5bcaad5c69e221ac1bb54aafc7bcbb8da943 /src
parentf204e2a5543257e77a4bc6ed666efa2f3c4ffabf (diff)
Update some comments
Diffstat (limited to 'src')
-rw-r--r--src/Values.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Values.ml b/src/Values.ml
index a0bd96c5..0239da5e 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -56,6 +56,10 @@ type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty }
We need to make this clear and more consistant.
So [symbolic_value] is actually a projector. TODO: rename to [symbolic_proj].
The kind of projector will then depend on the context.
+ Actually, maybe we shouldn't use this type. Or for abstractions we should
+ use different types. Something like:
+ - [proj_borrows] for values
+ - [aproj_loans], [aproj_borrows] for avalues
*)
(** TODO: make it clear that complementary projectors are projectors on borrows.