From 08e7ec2c48c5ca666ad42b5f969576e6aa43d2ea Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 22 Aug 2013 14:29:58 +0000
Subject: 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
---
 interp/coqlib.ml    | 3 +++
 interp/coqlib.mli   | 2 ++
 interp/dumpglob.ml  | 8 +++++---
 interp/dumpglob.mli | 3 +--
 4 files changed, 11 insertions(+), 5 deletions(-)

(limited to 'interp')

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
-- 
cgit v1.2.3