2 files changed, 28 insertions, 0 deletions
diff --git a/lib/options.ml b/lib/options.ml
index 8d49d6b75..f1e40a89e 100644
--- a/lib/options.ml
+++ b/lib/options.ml
@@ -54,3 +54,24 @@ let print_hyps_limit () = !print_hyps_limit
 let unsafe_set = ref Stringset.empty
 let add_unsafe s = unsafe_set := Stringset.add s !unsafe_set
 let is_unsafe s = Stringset.mem s !unsafe_set
+
+
+(* Dump of globalization (to be used by coqdoc) *)
+
+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_append; Open_creat] in
+    let c = open_out_gen mode 0o666 !dump_file in
+    output_string c (Buffer.contents dump_buffer);
+    close_out c
+  end
+
+let _ = at_exit dump_it
diff --git a/lib/options.mli b/lib/options.mli
index e8f7a2780..efc8617de 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -34,3 +34,10 @@ val print_hyps_limit : unit -> int option
 
 val add_unsafe : string -> unit
 val is_unsafe : string -> bool
+
+(* Dump of globalization (to be used by coqdoc) *)
+
+val dump : bool ref
+val dump_into_file : string -> unit
+val dump_string : string -> unit
+