From 59c9403ceb09a35ed219b522e9f5abdb50615d76 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 12 Apr 2012 20:49:01 +0000 Subject: 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 --- library/goptions.ml | 4 ++-- library/goptions.mli | 4 ++-- library/goptionstyp.mli | 26 -------------------------- library/library.ml | 10 +++++----- library/library.mli | 16 ++++++++-------- 5 files changed, 17 insertions(+), 43 deletions(-) delete mode 100644 library/goptionstyp.mli (limited to 'library') diff --git a/library/goptions.ml b/library/goptions.ml index 30804fa5f1..1a490c8cef 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 979bca2d27..bf894d9c89 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 541a1470c7..0000000000 --- a/library/goptionstyp.mli +++ /dev/null @@ -1,26 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 c569ff4851..95e4a6eb0e 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. } *) -- cgit v1.2.3