modules et coqc

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

4 files changed, 10 insertions, 6 deletions

diff --git a/lib/options.ml b/lib/options.ml
index 26869e7adc..fdfec98d08 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -15,7 +15,7 @@ let emacs_str s = if !print_emacs then s else ""
 let silent = ref false
 let make_silent flag = silent := flag; ()
 let is_silent () = !silent
-let verbose () = not !silent
+let is_verbose () = not !silent
 
 let silently f x =
   let oldsilent = !silent in
diff --git a/lib/options.mli b/lib/options.mli
index dc6b5b9824..25c194106b 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -12,7 +12,7 @@ val emacs_str : string -> string
 
 val make_silent : bool -> unit
 val is_silent : unit -> bool
-val verbose : unit -> bool
+val is_verbose : unit -> bool
 val silently : ('a -> 'b) -> 'a -> 'b
 
 val set_print_hyps_limit : int -> unit
diff --git a/lib/system.ml b/lib/system.ml
index 5422bc4659..aed203b206 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -101,13 +101,15 @@ let try_remove f =
   with _ -> mSGNL [< 'sTR"Warning: " ; 'sTR"Could not remove file " ;
                      'sTR f ; 'sTR" which is corrupted !!" >]
 
+let marshal_out ch v = Marshal.to_channel ch v [Marshal.Closures]
+let marshal_in ch = Marshal.from_channel ch
+
 exception Bad_magic_number of string
 
 let (raw_extern_intern :
      int -> string -> 
        (string -> string * out_channel) * (string -> string * in_channel))
   = fun magic suffix ->
-
     let extern_state name = 
       let (_,channel) as filec =
 	open_trapping_failure (fun n -> n,open_out_bin n) name suffix in
@@ -125,13 +127,12 @@ let (raw_extern_intern :
 let (extern_intern :
      int -> string -> (string -> 'a -> unit) * (string -> 'a))
   = fun magic suffix ->
-
     let (raw_extern,raw_intern) = raw_extern_intern magic suffix in
     let extern_state name val_0 = 
       try
 	let (fname,channel) = raw_extern name in
       	try
-          output_value channel val_0;
+          marshal_out channel val_0;
           close_out channel
       	with e -> 
 	  begin try_remove fname; raise e end
@@ -140,7 +141,7 @@ let (extern_intern :
   and intern_state name = 
     try
       let (fname,channel) = raw_intern name in
-      let v = input_value channel in
+      let v = marshal_in channel in
       close_in channel; 
       v
     with Sys_error s -> error("System error: " ^ s)
diff --git a/lib/system.mli b/lib/system.mli
index e3fd5978c3..3d355e8438 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -28,6 +28,9 @@ val find_file_in_path : string -> string
   and a suffix. The intern functions raise the exception [Bad_magic_number]
   when the check fails, with the full file name. *)
 
+val marshal_out : out_channel -> 'a -> unit
+val marshal_in : in_channel -> 'a
+
 exception Bad_magic_number of string
 
 val raw_extern_intern : int -> string ->