2 files changed, 21 insertions, 0 deletions
diff --git a/lib/options.ml b/lib/options.ml
index 2e8c535173..ec9f0cb13d 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -108,3 +108,14 @@ let dump_it () =
 
 let _ = at_exit dump_it
 
+(* Options for the virtual machine *)
+
+let print_bytecodes = ref false 
+let set_print_bytecodes b = print_bytecodes := b
+let print_bytecodes _ = !print_bytecodes
+
+
+let boxed_definitions = ref true
+let set_boxed_definitions b = boxed_definitions := b
+let boxed_definitions _ = !boxed_definitions 
+ 
diff --git a/lib/options.mli b/lib/options.mli
index d999425e92..bf935c76d3 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -62,3 +62,13 @@ val dump : bool ref
 val dump_into_file : string -> unit
 val dump_string : string -> unit
 
+(* Options for the virtual machine *)
+
+
+val set_print_bytecodes : bool -> unit
+val print_bytecodes : unit -> bool
+
+val set_boxed_definitions : bool -> unit
+val boxed_definitions : unit -> bool
+
+