Modulification of dir_path

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 10 deletions

diff --git a/library/nametab.mli b/library/nametab.mli
index 8a18166a9..188e2dcee 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]
+         [module_path], [Dir_path.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].
+     [full_user_name] can either be a [full_path] or a [Dir_path.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 -> global_dir_reference -> unit
+val push_dir : visibility -> Dir_path.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
+val locate_section : qualid -> Dir_path.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 -> bool
-val exists_section : dir_path -> bool (** deprecated synonym of [exists_dir] *)
-val exists_module : dir_path -> bool (** deprecated synonym of [exists_dir] *)
+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] *)
 
 (** {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
+val full_name_module : qualid -> Dir_path.t
 
 (** {6 Reverse lookup }
   Finding user names corresponding to the given
@@ -142,13 +142,13 @@ val full_name_module : qualid -> dir_path
 
 val path_of_syndef : syndef_name -> full_path
 val path_of_global : global_reference -> full_path
-val dirpath_of_module : module_path -> dir_path
+val dirpath_of_module : module_path -> Dir_path.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
+val dirpath_of_global : global_reference -> Dir_path.t
 val basename_of_global : global_reference -> Id.t
 
 (** Printing of global references using names as short as possible *)