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

2 files changed, 19 insertions, 18 deletions

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index bc840d2d9f..c7e7044df3 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -195,12 +195,13 @@ let coqdep () =
     add_rec_dir add_known "theories" ["Coq"];
     add_rec_dir add_known "plugins" ["Coq"]
   end else begin
-    let coqlib = Envars.coqlib () in
+    let coqlib = Envars.coqlib Errors.error in
     add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"];
     add_rec_dir add_coqlib_known (coqlib//"plugins") ["Coq"];
     let user = coqlib//"user-contrib" in
     if Sys.file_exists user then add_rec_dir add_coqlib_known user [];
-    List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.xdg_dirs;
+    List.iter (fun s -> add_rec_dir add_coqlib_known s [])
+      (Envars.xdg_dirs (fun x -> Pp.msg_warning (Pp.str x)));
     List.iter (fun s -> add_rec_dir add_coqlib_known s []) Envars.coqpath;
   end;
   List.iter (fun (f,d) -> add_mli_known f d) !mliAccu;
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index f2255981a7..31303b5bab 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -15,28 +15,28 @@ let coqtop = ref (stdin, stdout)
 let p = Xml_parser.make ()
 let () = Xml_parser.check_eof p false
 
-let eval_call (call:'a Ide_intf.call) =
-  prerr_endline (Ide_intf.pr_call call);
-  let xml_query = Ide_intf.of_call call in
+let eval_call (call:'a Serialize.call) =
+  prerr_endline (Serialize.pr_call call);
+  let xml_query = Serialize.of_call call in
   Xml_utils.print_xml (snd !coqtop) xml_query;
   flush (snd !coqtop);
   let xml_answer = Xml_parser.parse p (Xml_parser.SChannel (fst !coqtop)) in
-  let res = Ide_intf.to_answer xml_answer in
-  prerr_endline (Ide_intf.pr_full_value call res);
+  let res = Serialize.to_answer xml_answer in
+  prerr_endline (Serialize.pr_full_value call res);
   match res with Interface.Fail _ -> exit 1 | _ -> ()
 
 let commands =
-  [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (true,false,s)));
-    "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (true,true,s)));
-    "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (false,false,s)));
-    "INTERP", (fun s -> eval_call (Ide_intf.interp (false,true,s)));
-    "REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s)));
-    "GOALS", (fun _ -> eval_call Ide_intf.goals);
-    "HINTS", (fun _ -> eval_call Ide_intf.hints);
-    "GETOPTIONS", (fun _ -> eval_call Ide_intf.get_options);
-    "STATUS", (fun _ -> eval_call Ide_intf.status);
-    "INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s));
-    "MKCASES", (fun s -> eval_call (Ide_intf.mkcases s));
+  [ "INTERPRAWSILENT", (fun s -> eval_call (Serialize.interp (true,false,s)));
+    "INTERPRAW", (fun s -> eval_call (Serialize.interp (true,true,s)));
+    "INTERPSILENT", (fun s -> eval_call (Serialize.interp (false,false,s)));
+    "INTERP", (fun s -> eval_call (Serialize.interp (false,true,s)));
+    "REWIND", (fun s -> eval_call (Serialize.rewind (int_of_string s)));
+    "GOALS", (fun _ -> eval_call Serialize.goals);
+    "HINTS", (fun _ -> eval_call Serialize.hints);
+    "GETOPTIONS", (fun _ -> eval_call Serialize.get_options);
+    "STATUS", (fun _ -> eval_call Serialize.status);
+    "INLOADPATH", (fun s -> eval_call (Serialize.inloadpath s));
+    "MKCASES", (fun s -> eval_call (Serialize.mkcases s));
     "#", (fun _ -> raise Comment);
   ]