From f987a343850df4602b3d8020395834d22eb1aea3 Mon Sep 17 00:00:00 2001
From: gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 12 Nov 2004 16:40:39 +0000
Subject: Changement dans les boxed values .

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/options.ml  | 11 +++++++++++
 lib/options.mli | 10 ++++++++++
 2 files changed, 21 insertions(+)

(limited to 'lib')

diff --git a/lib/options.ml b/lib/options.ml
index 2e8c53517..ec9f0cb13 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 d999425e9..bf935c76d 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
+
+ 
-- 
cgit v1.2.3