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

1 files changed, 4 insertions, 1 deletions

diff --git a/lib/envars.mli b/lib/envars.mli
index c0142a8d76..19ba8d2c02 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -25,7 +25,10 @@ val expand_path_macros : warn:(string -> unit) -> string -> string
 val home : warn:(string -> unit) -> string
 
 (** [coqlib] is the path to the Coq library. *)
-val coqlib : fail:(string -> string) -> string
+val coqlib : unit -> string
+
+(** [set_coqlib] must be runned once before any access to [coqlib] *)
+val set_coqlib : fail:(string -> string) -> unit
 
 (** [docdir] is the path to the Coq documentation. *)
 val docdir : unit -> string