aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/lib.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-19 20:27:51 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-19 20:27:51 +0000
commit248728628f5da946f96c22ba0a0e7e9b33019382 (patch)
tree905dbbafa65dd7bf02823318326be2ca389f833f /library/lib.mli
parent3889c9a9e7d017ef2eea647d8c17d153a0b90083 (diff)
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
Diffstat (limited to 'library/lib.mli')
-rw-r--r--library/lib.mli26
1 files changed, 13 insertions, 13 deletions
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 } *)