Add a Set Dump Bytecode command for debugging purposes.

Prints the VM bytecode produced by compilation of a constant or a call to
vm_compute.

1 files changed, 4 insertions, 4 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 80fe26a817..8d9f8f52c8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1435,10 +1435,10 @@ let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
-      optname  = "printing of universes";
-      optkey   = ["Printing";"Universes"];
-      optread  = (fun () -> !Constrextern.print_universes);
-      optwrite = (fun b -> Constrextern.print_universes:=b) }
+      optname  = "dumping bytecode after compilation";
+      optkey   = ["Dump";"Bytecode"];
+      optread  = Flags.get_dump_bytecode;
+      optwrite = Flags.set_dump_bytecode }
 
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)