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, 2 deletions

diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 39a8ede9a9..0ab732da21 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -72,10 +72,10 @@ let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
    below (for accessing the corresponding .cmi). *)
 
 let src_dirs =
-  [ []; ["lib"]; ["toplevel"]; ["kernel";"byterun"]  ]
+  [ []; ["lib"]; ["toplevel"]; ["kernel/byterun"]  ]
 
 let includes () =
-  let coqlib = if !Flags.boot then "." else Envars.coqlib ~fail:Errors.error in
+  let coqlib = if !Flags.boot then "." else Envars.coqlib () in
   let mkdir d = "\"" ^ List.fold_left Filename.concat coqlib d ^ "\"" in
   (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs [])
   @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""]
@@ -259,6 +259,7 @@ let create_tmp_main_file modules =
 (* main part *)
 let main () =
   let (options, userfiles) = parse_args () in
+  let () = Envars.set_coqlib ~fail:Errors.error in
   (* which ocaml command to invoke *)
   let camlbin = Envars.camlbin () in
   let prog =