Misc changes around coqtop.ml :

 - Revised Coqtop.parse_args in a cleaner and lighter style
 - Improved error message in case of argument parse failure:
   * tell which option is expecting a related argument
   * in case of unknown options, warn about them all at once
   * do not hide the previous error messages by filling the
     screen with usage(). Instead, suggest the use of --help.
 - Specialized boolean config field Coq_config.arch_is_win32
 - Faster Envars.coqlib, which is back to (unit->string), and
   just access Flags.coqlib. Caveat: it must be initialized once
   via Envars.set_coqlib
 - Avoid keeping an opened channel to the "revision" file
 - Direct load of theories/init/prelude.vo, no detour via Loadpath

Beware : ./configure must be runned after this commit

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

4 files changed, 11 insertions, 5 deletions

diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 2256764a36..aac7f9a280 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -117,6 +117,9 @@ let init_modules = [
   init_dir@["Wf"]
 ]
 
+let prelude_module_name = init_dir@["Prelude"]
+let prelude_module = make_dir prelude_module_name
+
 let logic_module_name = init_dir@["Logic"]
 let logic_module = make_dir logic_module_name
 
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index b8e461665a..9e0cfadae9 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -54,6 +54,8 @@ val check_required_library : string list -> unit
 (** {6 Global references } *)
 
 (** Modules *)
+val prelude_module : DirPath.t
+
 val logic_module : DirPath.t
 val logic_module_name : string list
 
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 74c60f75be..1a44fac6cf 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -30,11 +30,13 @@ let dump () = !glob_output != NoGlob
 
 let noglob () = glob_output := NoGlob
 
-let dump_to_stdout () = glob_output := StdOut; glob_file := Pervasives.stdout
-
 let dump_to_dotglob () = glob_output := MultFiles
 
-let dump_into_file f = glob_output := File f; open_glob_file f
+let dump_into_file f =
+  if String.equal f "stdout" then
+    (glob_output := StdOut; glob_file := Pervasives.stdout)
+  else
+    (glob_output := File f; open_glob_file f)
 
 let dump_string s =
   if dump () then Pervasives.output_string !glob_file s
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index edea94f0c0..37370f6e1c 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -15,8 +15,7 @@ val end_dump_glob : unit -> unit
 val dump : unit -> bool
 
 val noglob : unit -> unit
-val dump_to_stdout : unit -> unit
-val dump_into_file : string -> unit
+val dump_into_file : string -> unit (** special handling of "stdout" *)
 val dump_to_dotglob : unit -> unit
 
 val pause : unit -> unit