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/nametab.mli | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'library/nametab.mli') diff --git a/library/nametab.mli b/library/nametab.mli index 188e2dcee..d561735fd 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -17,7 +17,7 @@ open Globnames qualified names (qualid). There are three classes of names: - 1a) internal kernel names: [kernel_name], [constant], [inductive], - [module_path], [Dir_path.t] + [module_path], [DirPath.t] - 1b) other internal names: [global_reference], [syndef_name], [extended_global_reference], [global_dir_reference], ... @@ -33,7 +33,7 @@ open Globnames Registers the [object_reference] to be referred to by the [full_user_name] (and its suffixes according to [visibility]). - [full_user_name] can either be a [full_path] or a [Dir_path.t]. + [full_user_name] can either be a [full_path] or a [DirPath.t]. } {- [exists : full_user_name -> bool] @@ -79,7 +79,7 @@ type visibility = Until of int | Exactly of int val push : visibility -> full_path -> global_reference -> unit val push_modtype : visibility -> full_path -> module_path -> unit -val push_dir : visibility -> Dir_path.t -> global_dir_reference -> unit +val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit type ltac_constant = kernel_name @@ -98,7 +98,7 @@ val locate_syndef : qualid -> syndef_name val locate_modtype : qualid -> module_path val locate_dir : qualid -> global_dir_reference val locate_module : qualid -> module_path -val locate_section : qualid -> Dir_path.t +val locate_section : qualid -> DirPath.t val locate_tactic : qualid -> ltac_constant (** These functions globalize user-level references into global @@ -123,15 +123,15 @@ val extended_global_of_path : full_path -> extended_global_reference val exists_cci : full_path -> bool val exists_modtype : full_path -> bool -val exists_dir : Dir_path.t -> bool -val exists_section : Dir_path.t -> bool (** deprecated synonym of [exists_dir] *) -val exists_module : Dir_path.t -> bool (** deprecated synonym of [exists_dir] *) +val exists_dir : DirPath.t -> bool +val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) +val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) (** {6 These functions locate qualids into full user names } *) val full_name_cci : qualid -> full_path val full_name_modtype : qualid -> full_path -val full_name_module : qualid -> Dir_path.t +val full_name_module : qualid -> DirPath.t (** {6 Reverse lookup } Finding user names corresponding to the given @@ -142,13 +142,13 @@ val full_name_module : qualid -> Dir_path.t val path_of_syndef : syndef_name -> full_path val path_of_global : global_reference -> full_path -val dirpath_of_module : module_path -> Dir_path.t +val dirpath_of_module : module_path -> DirPath.t val path_of_tactic : ltac_constant -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) -val dirpath_of_global : global_reference -> Dir_path.t +val dirpath_of_global : global_reference -> DirPath.t val basename_of_global : global_reference -> Id.t (** Printing of global references using names as short as possible *) -- cgit v1.2.3