summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-02-09 21:55:59 +0100
committerSon Ho2022-02-09 21:55:59 +0100
commit337caa185fa51ab81fa896db0dc9671c7599f4fa (patch)
tree8fca08b5f0a94a26589c96ea31ea385a535b5612 /src
parent6b05d49e030e1fba51698b34ed06c3436c23b8a6 (diff)
Add a comment
Diffstat (limited to 'src')
-rw-r--r--src/PureMicroPasses.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index e53bc912..dd2401b9 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -935,7 +935,8 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
("inline_useless_var_assignments:\n\n" ^ fun_def_to_string ctx def
^ "\n"));
- (* Eliminate the box functions *)
+ (* Eliminate the box functions - note that the "box" types were eliminated
+ * during the symbolic to pure phase: see the comments for [eliminate_box_functions] *)
let def = eliminate_box_functions ctx def in
log#ldebug
(lazy