From 248728628f5da946f96c22ba0a0e7e9b33019382 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 19 Feb 2013 20:27:51 +0000 Subject: Dir_path --> DirPath Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/library.mli | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) (limited to 'library/library.mli') diff --git a/library/library.mli b/library/library.mli index 6cf4107cb..11253087a 100644 --- a/library/library.mli +++ b/library/library.mli @@ -24,7 +24,7 @@ open Libobject (** Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) val require_library : qualid located list -> bool option -> unit -val require_library_from_dirpath : (Dir_path.t * string) list -> bool option -> unit +val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit val require_library_from_file : Id.t option -> CUnix.physical_path -> bool option -> unit @@ -34,40 +34,40 @@ val require_library_from_file : val import_module : bool -> qualid located -> unit (** {6 Start the compilation of a library } *) -val start_library : string -> Dir_path.t * string +val start_library : string -> DirPath.t * string (** {6 End the compilation of a library and save it to a ".vo" file } *) -val save_library_to : Dir_path.t -> string -> unit +val save_library_to : DirPath.t -> string -> unit (** {6 Interrogate the status of libraries } *) (** - Tell if a library is loaded or opened *) -val library_is_loaded : Dir_path.t -> bool -val library_is_opened : Dir_path.t -> bool +val library_is_loaded : DirPath.t -> bool +val library_is_opened : DirPath.t -> bool (** - Tell which libraries are loaded or imported *) -val loaded_libraries : unit -> Dir_path.t list -val opened_libraries : unit -> Dir_path.t list +val loaded_libraries : unit -> DirPath.t list +val opened_libraries : unit -> DirPath.t list (** - Return the full filename of a loaded library. *) -val library_full_filename : Dir_path.t -> string +val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit (** {6 Hook for the xml exportation of libraries } *) -val set_xml_require : (Dir_path.t -> unit) -> unit +val set_xml_require : (DirPath.t -> unit) -> unit (** {6 ... } *) (** Global load paths: a load path is a physical path in the file - system; to each load path is associated a Coq [Dir_path.t] (the "logical" + system; to each load path is associated a Coq [DirPath.t] (the "logical" path of the physical path) *) val get_load_paths : unit -> CUnix.physical_path list -val get_full_load_paths : unit -> (CUnix.physical_path * Dir_path.t) list -val add_load_path : bool -> CUnix.physical_path * Dir_path.t -> unit +val get_full_load_paths : unit -> (CUnix.physical_path * DirPath.t) list +val add_load_path : bool -> CUnix.physical_path * DirPath.t -> unit val remove_load_path : CUnix.physical_path -> unit -val find_logical_path : CUnix.physical_path -> Dir_path.t +val find_logical_path : CUnix.physical_path -> DirPath.t val is_in_load_paths : CUnix.physical_path -> bool (** {6 Locate a library in the load paths } *) @@ -76,8 +76,8 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - bool -> qualid -> library_location * Dir_path.t * CUnix.physical_path -val try_locate_qualified_library : qualid located -> Dir_path.t * string + bool -> qualid -> library_location * DirPath.t * CUnix.physical_path +val try_locate_qualified_library : qualid located -> DirPath.t * string (** {6 Statistics: display the memory use of a library. } *) -val mem : Dir_path.t -> Pp.std_ppcmds +val mem : DirPath.t -> Pp.std_ppcmds -- cgit v1.2.3