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, 11 insertions, 7 deletions

diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 070778fb2..b356ac537 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -25,12 +25,14 @@ let out_to = ref MultFiles
 
 let out_channel = ref stdout
 
+let ( / ) = Filename.concat
+
 let coqdoc_out f =
   if !output_dir <> "" && Filename.is_relative f then
     if not (Sys.file_exists !output_dir) then
       (Printf.eprintf "No such directory: %s\n" !output_dir; exit 1)
     else
-      Filename.concat !output_dir f
+      !output_dir / f
   else
     f
 
@@ -73,15 +75,17 @@ let normalize_filename f =
 let guess_coqlib () =
   let file = "theories/Init/Prelude.vo" in
   match Coq_config.coqlib with
-    | Some coqlib when Sys.file_exists (Filename.concat coqlib file) ->
-      coqlib
+    | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib
     | Some _ | None ->
       let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
       let prefix = Filename.dirname coqbin in
-      let rpath = if Coq_config.local then [] else
-	  (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
-      let coqlib = List.fold_left Filename.concat prefix rpath in
-      if Sys.file_exists (Filename.concat coqlib file) then coqlib
+      let rpath =
+        if Coq_config.local then []
+        else if Coq_config.arch_is_win32 then ["lib"]
+        else ["lib/coq"]
+      in
+      let coqlib = List.fold_left (/) prefix rpath in
+      if Sys.file_exists (coqlib / file) then coqlib
       else prefix
 
 let header_trailer = ref true