From 5f7adad4af7d526aed3a97f8b24b2d9811f9fea7 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 23 Jun 2015 18:02:30 +0200
Subject: 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.
---
 lib/flags.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib/flags.ml')

diff --git a/lib/flags.ml b/lib/flags.ml
index 009caa9dee..ab4ac03f80 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -215,3 +215,7 @@ let native_compiler = ref false
 let print_mod_uid = ref false
 
 let tactic_context_compat = ref false
+
+let dump_bytecode = ref false
+let set_dump_bytecode = (:=) dump_bytecode
+let get_dump_bytecode () = !dump_bytecode
-- 
cgit v1.2.3