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/lib.mli | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'library/lib.mli') diff --git a/library/lib.mli b/library/lib.mli index 13a79caf1..1ea76f1ad 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -72,15 +72,15 @@ val contents_after : Libnames.object_name option -> library_segment (** {6 Functions relative to current path } *) (** User-side names *) -val cwd : unit -> Names.Dir_path.t -val cwd_except_section : unit -> Names.Dir_path.t -val current_dirpath : bool -> Names.Dir_path.t (* false = except sections *) +val cwd : unit -> Names.DirPath.t +val cwd_except_section : unit -> Names.DirPath.t +val current_dirpath : bool -> Names.DirPath.t (* false = except sections *) val make_path : Names.Id.t -> Libnames.full_path val make_path_except_section : Names.Id.t -> Libnames.full_path val path_of_include : unit -> Libnames.full_path (** Kernel-side names *) -val current_prefix : unit -> Names.module_path * Names.Dir_path.t +val current_prefix : unit -> Names.module_path * Names.DirPath.t val make_kn : Names.Id.t -> Names.kernel_name val make_con : Names.Id.t -> Names.constant @@ -124,19 +124,19 @@ val end_modtype : (** {6 Compilation units } *) -val start_compilation : Names.Dir_path.t -> Names.module_path -> unit -val end_compilation : Names.Dir_path.t -> Libnames.object_prefix * library_segment +val start_compilation : Names.DirPath.t -> Names.module_path -> unit +val end_compilation : Names.DirPath.t -> Libnames.object_prefix * library_segment -(** The function [library_dp] returns the [Dir_path.t] of the current +(** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) -val library_dp : unit -> Names.Dir_path.t +val library_dp : unit -> Names.DirPath.t (** Extract the library part of a name even if in a section *) -val dp_of_mp : Names.module_path -> Names.Dir_path.t -val split_mp : Names.module_path -> Names.Dir_path.t * Names.Dir_path.t -val split_modpath : Names.module_path -> Names.Dir_path.t * Names.Id.t list -val library_part : Globnames.global_reference -> Names.Dir_path.t -val remove_section_part : Globnames.global_reference -> Names.Dir_path.t +val dp_of_mp : Names.module_path -> Names.DirPath.t +val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t +val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list +val library_part : Globnames.global_reference -> Names.DirPath.t +val remove_section_part : Globnames.global_reference -> Names.DirPath.t (** {6 Sections } *) -- cgit v1.2.3