lib directory is cut in 2 cma.

 - Clib that does not depend on camlpX and is made to be shared by all coq
   tools/scripts/...
 - Lib that is Coqtop specific

As a side effect for the build system :
 - Coq_config is in Clib and does not appears in makefiles
 - only the BEST version of coqc and coqmktop is made
 - ocamlbuild build system fails latter but is still broken

(ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 10 insertions, 8 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 6f01107f5c..3194b26813 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -54,7 +54,7 @@ type library_disk = {
 
 type library_t = {
   library_name : compilation_unit_name;
-  library_filename : System.physical_path;
+  library_filename : CUnix.physical_path;
   library_compiled : Safe_typing.compiled_library;
   library_deps : (compilation_unit_name * Digest.t) list;
   library_digest : Digest.t }
@@ -114,7 +114,7 @@ let check_one_lib admit (dir,m) =
 
 type logical_path = dir_path
 
-let load_paths = ref ([],[] : System.physical_path list * logical_path list)
+let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list)
 
 let get_load_paths () = fst !load_paths
 
diff --git a/checker/check.mllib b/checker/check.mllib
index 99b952a389..2cd86355fc 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -9,6 +9,7 @@ Errors
 Util
 Option
 Hashcons
+CUnix
 System
 Envars
 Predicate
diff --git a/checker/checker.ml b/checker/checker.ml
index 4da4d14e13..44a77836cd 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -43,7 +43,7 @@ let (/) = Filename.concat
 
 let get_version_date () =
   try
-    let coqlib = Envars.coqlib () in
+    let coqlib = Envars.coqlib error in
     let ch = open_in (Filename.concat coqlib "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
@@ -101,7 +101,7 @@ let set_rec_include d p =
 
 (* Initializes the LoadPath *)
 let init_load_path () =
-  let coqlib = Envars.coqlib () in
+  let coqlib = Envars.coqlib error in
   let user_contrib = coqlib/"user-contrib" in
   let xdg_dirs = Envars.xdg_dirs in
   let coqpath = Envars.coqpath in
@@ -115,7 +115,8 @@ let init_load_path () =
   if Sys.file_exists user_contrib then
     add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
   (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
-  List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) xdg_dirs;
+  List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix)
+    (xdg_dirs ~warn:(fun x -> msg_warning (str x)));
   (* then directories in COQPATH *)
   List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
   (* then current directory *)
@@ -309,7 +310,7 @@ let parse_args argv =
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-where" :: _ ->
-        print_endline (Envars.coqlib ()); exit 0
+        print_endline (Envars.coqlib error); exit 0
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index cd2c06d20e..b7d7d04cc6 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -19,9 +19,9 @@ type compiled_library
 
 val set_engagement : Declarations.engagement -> unit
 val import         :
-  System.physical_path -> compiled_library -> Digest.t -> unit
+  CUnix.physical_path -> compiled_library -> Digest.t -> unit
 val unsafe_import  :
-  System.physical_path -> compiled_library -> Digest.t -> unit
+  CUnix.physical_path -> compiled_library -> Digest.t -> unit
 
 (** Store the body of modules' opaque constants inside a table.