aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
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 415e4399a..5da131020 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 c82410f07..bc07dec80 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