summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-12-08 15:54:09 +0100
committerSon Ho2021-12-08 15:54:09 +0100
commit9826e2de450b4c20405e5c4779b45bba5b2693db (patch)
tree7cd818d2b7f2bcb9dda0928c3235e8bc9f75c9c8
parent4b2018c4dfb1335b9267eaf21fcb93ed5acbd00e (diff)
Remove a TODO
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 8eebd241..560cf58b 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -10,7 +10,6 @@ module L = Logging
open TypesUtils
open ValuesUtils
-(* TODO: Change state-passing style to : st -> ... -> (st, v) *)
(* TODO: check that the value types are correct when evaluating *)
(* TODO: for debugging purposes, we might want to put use eval_ctx everywhere
(rather than only env) *)