aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorMaxime Dénès2018-02-24 09:33:03 +0100
committerMaxime Dénès2018-02-24 09:33:03 +0100
commitbd41af496fd09d6ecd965190cad2873f1cd6b029 (patch)
tree029c44d509cdaba200db07dfed61adb55b237f9e /lib
parentc4aeaa7aedb04bf156a4946b05bad8f66d5eec69 (diff)
parent557c5a2938f16c0601f5a0323c66b78d2da01ee9 (diff)
Merge PR #6784: New IR in VM: Clambda
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml4
-rw-r--r--lib/flags.mli5
2 files changed, 9 insertions, 0 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 415e4399ad..5da1310206 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -170,3 +170,7 @@ let profile_ltac_cutoff = ref 2.0
let dump_bytecode = ref false
let set_dump_bytecode = (:=) dump_bytecode
let get_dump_bytecode () = !dump_bytecode
+
+let dump_lambda = ref false
+let set_dump_lambda = (:=) dump_lambda
+let get_dump_lambda () = !dump_lambda
diff --git a/lib/flags.mli b/lib/flags.mli
index c82410f07c..bc07dec804 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -132,3 +132,8 @@ val profile_ltac_cutoff : float ref
val dump_bytecode : bool ref
val set_dump_bytecode : bool -> unit
val get_dump_bytecode : unit -> bool
+
+(** Dump the VM lambda code after compilation (for debugging purposes) *)
+val dump_lambda : bool ref
+val set_dump_lambda : bool -> unit
+val get_dump_lambda : unit -> bool