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

5 files changed, 17 insertions, 43 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 30804fa5f..1a490c8ce 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -18,9 +18,9 @@ open Term
 open Nametab
 open Mod_subst
 
-open Goptionstyp
+open Interface
 
-type option_name = Goptionstyp.option_name
+type option_name = Interface.option_name
 
 (****************************************************************************)
 (* 0- Common things                                                         *)
diff --git a/library/goptions.mli b/library/goptions.mli
index 979bca2d2..bf894d9c8 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -52,7 +52,7 @@ open Term
 open Nametab
 open Mod_subst
 
-type option_name = Goptionstyp.option_name
+type option_name = Interface.option_name
 
 (** {6 Tables. } *)
 
@@ -165,7 +165,7 @@ val set_string_option_value : option_name -> string -> unit
 
 val print_option_value : option_name -> unit
 
-val get_tables : unit -> Goptionstyp.option_state OptionMap.t
+val get_tables : unit -> Interface.option_state OptionMap.t
 val print_tables : unit -> unit
 
 val error_undeclared_key : option_name -> 'a
diff --git a/library/goptionstyp.mli b/library/goptionstyp.mli
deleted file mode 100644
index 541a1470c..000000000
--- a/library/goptionstyp.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Some types used in the generic option mechanism (Goption) *)
-
-(** Placing them here in a pure interface avoid some dependency issues
-    when compiling CoqIDE *)
-
-type option_name = string list
-
-type option_value =
-  | BoolValue   of bool
-  | IntValue    of int option
-  | StringValue of string
-
-type option_state = {
-  opt_sync  : bool;
-  opt_depr  : bool;
-  opt_name  : string;
-  opt_value : option_value;
-}
diff --git a/library/library.ml b/library/library.ml
index e2adb3fb9..66bca4f1b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -23,19 +23,19 @@ open Nametab
 
 type logical_path = dir_path
 
-let load_paths = ref ([] : (System.physical_path * logical_path * bool) list)
+let load_paths = ref ([] : (CUnix.physical_path * logical_path * bool) list)
 
 let get_load_paths () = List.map pi1 !load_paths
 
 let find_logical_path phys_dir =
-  let phys_dir = System.canonical_path_name phys_dir in
+  let phys_dir = CUnix.canonical_path_name phys_dir in
   match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with
   | [_,dir,_] -> dir
   | [] -> Nameops.default_root_prefix
   | l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
 let is_in_load_paths phys_dir =
-  let dir = System.canonical_path_name phys_dir in
+  let dir = CUnix.canonical_path_name phys_dir in
   let lp = get_load_paths () in
   let check_p = fun p -> (String.compare dir p) == 0 in
     List.exists check_p lp
@@ -44,13 +44,13 @@ let remove_load_path dir =
   load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths
 
 let add_load_path isroot (phys_path,coq_path) =
-  let phys_path = System.canonical_path_name phys_path in
+  let phys_path = CUnix.canonical_path_name phys_path in
     match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with
       | [_,dir,_] ->
 	  if coq_path <> dir
             (* If this is not the default -I . to coqtop *)
             && not
-            (phys_path = System.canonical_path_name Filename.current_dir_name
+            (phys_path = CUnix.canonical_path_name Filename.current_dir_name
 		&& coq_path = Nameops.default_root_prefix)
 	  then
 	    begin
diff --git a/library/library.mli b/library/library.mli
index c569ff485..95e4a6eb0 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -26,7 +26,7 @@ open Libobject
 val require_library : qualid located list -> bool option -> unit
 val require_library_from_dirpath : (dir_path * string) list -> bool option -> unit
 val require_library_from_file :
-  identifier option -> System.physical_path -> bool option -> unit
+  identifier option -> CUnix.physical_path -> bool option -> unit
 
 (** {6 ... } *)
 (** Open a module (or a library); if the boolean is true then it's also
@@ -63,12 +63,12 @@ val set_xml_require : (dir_path -> unit) -> unit
     system; to each load path is associated a Coq [dir_path] (the "logical"
     path of the physical path) *)
 
-val get_load_paths : unit -> System.physical_path list
-val get_full_load_paths : unit -> (System.physical_path * dir_path) list
-val add_load_path : bool -> System.physical_path * dir_path -> unit
-val remove_load_path : System.physical_path -> unit
-val find_logical_path : System.physical_path -> dir_path
-val is_in_load_paths : System.physical_path -> bool
+val get_load_paths : unit -> CUnix.physical_path list
+val get_full_load_paths : unit -> (CUnix.physical_path * dir_path) list
+val add_load_path : bool -> CUnix.physical_path * dir_path -> unit
+val remove_load_path : CUnix.physical_path -> unit
+val find_logical_path : CUnix.physical_path -> dir_path
+val is_in_load_paths : CUnix.physical_path -> bool
 
 (** {6 Locate a library in the load paths } *)
 exception LibUnmappedDir
@@ -76,7 +76,7 @@ exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
 val locate_qualified_library :
-  bool -> qualid -> library_location * dir_path * System.physical_path
+  bool -> qualid -> library_location * dir_path * CUnix.physical_path
 val try_locate_qualified_library : qualid located -> dir_path * string
 
 (** {6 Statistics: display the memory use of a library. } *)