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, 3 insertions, 4 deletions

diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 6b2b4aa7c..c9da5222f 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -32,13 +32,12 @@ let open_header = List.map mk_open open_header
 let compiler_name =
   Filename.quote (if Dynlink.is_native then ocamlopt () else ocamlc ())
 
-let ( / ) a b = Filename.concat a b
+let ( / ) = Filename.concat
 
 (* We have to delay evaluation of include_dirs because coqlib cannot be guessed
 until flags have been properly initialized *)
-let include_dirs () = [Filename.temp_dir_name;
-                    coqlib ~fail:Errors.error / "kernel";
-                    coqlib ~fail:Errors.error / "library"]
+let include_dirs () =
+  [Filename.temp_dir_name; coqlib () / "kernel"; coqlib () / "library"]
 
 (* Pointer to the function linking an ML object into coq's toplevel *)
 let load_obj = ref (fun x -> () : string -> unit)