Changement dans les boxed values .

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 38 insertions, 8 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index e0339768e..3d468d328 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -270,7 +270,7 @@ let build_id_coercion idf_opt source =
       { const_entry_body = mkCast (val_f, typ_f);
 	const_entry_type = Some typ_f;
         const_entry_opaque = false;
-	const_entry_boxed = false} in
+	const_entry_boxed = Options.boxed_definitions()} in
   let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
   ConstRef kn
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index a0cf3c40e..8eaab89d3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -198,7 +198,7 @@ let declare_one_elimination ind =
         { const_entry_body = c;
           const_entry_type = t;
           const_entry_opaque = false;
-	  const_entry_boxed = true }, 
+	  const_entry_boxed = Options.boxed_definitions() }, 
        Decl_kinds.IsDefinition) in
     definition_message id;
     kn
@@ -620,7 +620,7 @@ let build_scheme lnamedepindsort =
     let ce = { const_entry_body = decl;
                const_entry_type = Some decltype;
                const_entry_opaque = false;
-	       const_entry_boxed = true } in
+	       const_entry_boxed = Options.boxed_definitions() } in
     let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
     ConstRef kn :: lrecref
   in 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 1a90139b4..c79ff8421 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -142,6 +142,14 @@ let re_exec is_ide =
     Unix.handle_unix_error (Unix.execvp newprog) Sys.argv
   end
 
+(*s options for the virtual machine *)
+let unb_val = ref (fun _ -> ())
+let unb_def = ref (fun _ -> ())
+let no_vm = ref (fun _ -> ())
+
+let set_vm_opt () =
+  !unb_val true;!unb_def false;!no_vm false
+
 (*s Parsing of the command line.
     We no longer use [Arg.parse], in order to use share [Usage.print_usage]
     between coqtop and coqc. *)
@@ -227,8 +235,13 @@ let parse_args is_ide =
     | "-unsafe" :: []       -> usage ()
 
     | "-debug" :: rem -> set_debug (); parse rem
-    | "-unboxed-values" :: rem -> Vm.set_transp_values true; parse rem
-    | "-no-vm" :: rem -> Reduction.use_vm := false;parse rem
+
+    | "-unboxed-values" :: rem -> 
+	unb_val := Vm.set_transp_values ; parse rem
+    | "-unboxed-definitions" :: rem ->
+	unb_def := Options.set_boxed_definitions; parse rem
+    | "-no-vm" :: rem -> no_vm := (fun b -> Reduction.use_vm := b);parse rem
+    | "-draw-vm-instr" :: rem -> Vm.set_drawinstr ();parse rem
     | "-emacs" :: rem -> Options.print_emacs := true; parse rem
 	  
     | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
@@ -297,6 +310,7 @@ let init is_ide =
       if_verbose print_header ();
       init_load_path ();
       inputstate ();
+      set_vm_opt ();
       engage ();
       if not !batch_mode then Declaremods.start_library !toplevel_name;
       init_library_roots ();
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c4e15b68b..e5a0681d8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -753,6 +753,14 @@ let _ =
 let _ =
   declare_bool_option 
     { optsync  = false;
+      optname  = "print the bytecode of global definitions";
+      optkey   = (SecondaryTable ("Print","Bytecode"));
+      optread  = Options.print_bytecodes;
+      optwrite = (fun b -> Options.set_print_bytecodes b) } 
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
       optname  = "use of virtual machine inside the kernel";
       optkey   = (SecondaryTable ("Virtual","Machine"));
       optread  = (fun () -> !Reduction.use_vm);
@@ -760,11 +768,19 @@ let _ =
 
 let _ =
   declare_bool_option 
-    { optsync  = false;
-      optname  = "transparent values for virtual machine";
+    { optsync  = true;
+      optname  = "use of boxed definitions";
+      optkey   = (SecondaryTable ("Boxed","Definitions"));
+      optread  = Options.boxed_definitions;
+      optwrite = (fun b -> Options.set_boxed_definitions b) } 
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "use of boxed values";
       optkey   = (SecondaryTable ("Boxed","Values"));
       optread  = Vm.transp_values;
-      optwrite = (fun b -> Vm.set_transp_values b) }
+      optwrite = (fun b -> Vm.set_transp_values (not b)) } 
 
 let _ =
   declare_int_option