summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-03 18:30:07 +0100
committerSon Ho2022-01-03 18:30:07 +0100
commite9f8d95e3f2618e776aa3cebadc469c523347f30 (patch)
tree4fa13ab9bced03b1f9c191f7753ab4eeeb4e50d3
parentfdc2f542725b0ee72afc619fe3b6c3e4b54e5b2e (diff)
Make a minor modification
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index e72ece58..5d07291c 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -2251,6 +2251,8 @@ type projection_access = {
We return the (eventually) updated value, the value we read at the end of
the place and the (eventually) updated environment.
+
+ TODO: use exceptions?
*)
let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
(* Function to (eventually) update the value we find *)