Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisation (add_glob* et dump_*)

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

2 files changed, 0 insertions, 20 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 68e287f693..f2ab87b4b7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -86,23 +86,6 @@ let is_unsafe s = Stringset.mem s !unsafe_set
 
 let noglob = ref false
 let dump = ref false
-let dump_file = ref ""
-let dump_into_file f = dump := true; dump_file := f
-
-let dump_buffer = Buffer.create 8192
-
-let dump_string = Buffer.add_string dump_buffer
-
-let dump_it () = 
-  if !dump then begin
-    let mode = [Open_wronly; Open_creat] in
-    let c = open_out_gen mode 0o666 !dump_file in
-    output_string c (Buffer.contents dump_buffer);
-    Buffer.clear dump_buffer;
-    close_out c
-  end
-
-let _ = at_exit dump_it
 
 (* Flags.for the virtual machine *)
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 08f9a279d1..4cab303815 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -61,9 +61,6 @@ val is_unsafe : string -> bool
 
 val noglob : bool ref
 val dump : bool ref
-val dump_into_file : string -> unit
-val dump_string : string -> unit
-val dump_it : unit -> unit
 
 (* Options for the virtual machine *)