summaryrefslogtreecommitdiff
path: root/src/InterpreterPaths.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/InterpreterPaths.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 491e4c21..bf039b52 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -730,6 +730,8 @@ let rec drop_borrows_loans_at_lplace (config : C.config) (p : E.place)
trait (i.e., by calling a dedicated function). This is why we added a parameter
to control this copy. Note that here by ADT we mean the user-defined ADTs
(not tuples or assumed types).
+
+ TODO: move
*)
let rec copy_value (allow_adt_copy : bool) (config : C.config)
(ctx : C.eval_ctx) (v : V.typed_value) : C.eval_ctx * V.typed_value =