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, 5 insertions, 5 deletions

diff --git a/library/global.mli b/library/global.mli
index fdada3f87..dac230a44 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -43,9 +43,9 @@ val push_named_def   : (Id.t * constr * types option) -> Univ.constraints
   functions verify that given names match those generated by kernel *)
 
 val add_constant :
-  dir_path -> Id.t -> global_declaration -> constant
+  Dir_path.t -> Id.t -> global_declaration -> constant
 val add_mind        :
-  dir_path -> Id.t -> mutual_inductive_entry -> mutual_inductive
+  Dir_path.t -> Id.t -> mutual_inductive_entry -> mutual_inductive
 
 val add_module      :
  Id.t -> module_entry -> inline -> module_path * delta_resolver
@@ -59,7 +59,7 @@ val add_constraints : constraints -> unit
 val set_engagement : engagement -> unit
 
 (** {6 Interactive modules and module types }
-   Both [start_*] functions take the [dir_path] argument to create a
+   Both [start_*] functions take the [Dir_path.t] argument to create a
    [mod_self_id]. This should be the name of the compilation unit. *)
 
 (** [start_*] functions return the [module_path] valid for components
@@ -90,8 +90,8 @@ val mind_of_delta_kn : kernel_name -> mutual_inductive
 val exists_objlabel  : label -> bool
 
 (** Compiled modules *)
-val start_library : dir_path -> module_path
-val export : dir_path -> module_path * compiled_library
+val start_library : Dir_path.t -> module_path
+val export : Dir_path.t -> module_path * compiled_library
 val import : compiled_library -> Digest.t -> module_path
 
 (** {6 ... } *)