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

19 files changed, 186 insertions, 188 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 3627df7fe..ee4656f75 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -53,7 +53,7 @@ type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (* opacity *)
   | SectionLocalAssum of types * bool (* Implicit status *)
 
-type variable_declaration = Dir_path.t * section_variable_entry * logical_kind
+type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
 let cache_variable ((sp,_),o) =
   match o with
diff --git a/library/declare.mli b/library/declare.mli
index 54a0160bf..bcb72be58 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -32,7 +32,7 @@ type section_variable_entry =
   | SectionLocalDef of constr * types option * bool (** opacity *)
   | SectionLocalAssum of types * bool (** Implicit status *)
 
-type variable_declaration = Dir_path.t * section_variable_entry * logical_kind
+type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
 val declare_variable : variable -> variable_declaration -> object_name
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index c96a9fbc0..591567fea 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -123,7 +123,7 @@ let modtab_objects =
 (* currently started interactive module (if any) - its arguments (if it
    is a functor) and declared output type *)
 let openmod_info =
-  ref ((MPfile(Dir_path.initial),[],None,[])
+  ref ((MPfile(DirPath.initial),[],None,[])
 	 : module_path *  MBId.t list *
            (module_struct_entry * int option) option *
 	   module_type_body list)
@@ -146,16 +146,16 @@ let _ = Summary.declare_summary "MODULE-INFO"
 	    Summary.init_function = (fun () ->
 				       modtab_substobjs := MPmap.empty;
 				       modtab_objects := MPmap.empty;
-				       openmod_info := ((MPfile(Dir_path.initial),
+				       openmod_info := ((MPfile(DirPath.initial),
 							 [],None,[]));
 				       library_cache := Dirmap.empty) }
 
 (* auxiliary functions to transform full_path and kernel_name given
-   by Lib into module_path and Dir_path.t needed for modules *)
+   by Lib into module_path and DirPath.t needed for modules *)
 
 let mp_of_kn kn =
   let mp,sec,l = repr_kn kn in
-    if Dir_path.is_empty sec then
+    if DirPath.is_empty sec then
       MPdot (mp,l)
     else
       anomaly (str "Non-empty section in module name!" ++ spc () ++ pr_kn kn)
@@ -246,8 +246,8 @@ let compute_visibility exists what i dir dirinfo =
       Nametab.Until i
 (*
 let do_load_and_subst_module i dir mp substobjs keep =
-  let prefix = (dir,(mp,Dir_path.empty)) in
-  let dirinfo = DirModule (dir,(mp,Dir_path.empty)) in
+  let prefix = (dir,(mp,DirPath.empty)) in
+  let dirinfo = DirModule (dir,(mp,DirPath.empty)) in
   let vis = compute_visibility false "load_and_subst" i dir dirinfo in
   let objects = compute_subst_objects mp substobjs resolver in
   Nametab.push_dir vis dir dirinfo;
@@ -263,8 +263,8 @@ let do_load_and_subst_module i dir mp substobjs keep =
 *)
 
 let do_module exists what iter_objects i dir mp substobjs keep=
-  let prefix = (dir,(mp,Dir_path.empty)) in
-  let dirinfo = DirModule (dir,(mp,Dir_path.empty)) in
+  let prefix = (dir,(mp,DirPath.empty)) in
+  let dirinfo = DirModule (dir,(mp,DirPath.empty)) in
   let vis = compute_visibility exists what i dir dirinfo in
     Nametab.push_dir vis dir dirinfo;
     modtab_substobjs := MPmap.add mp substobjs !modtab_substobjs;
@@ -314,7 +314,7 @@ let cache_keep _ = anomaly (Pp.str "This module should not be cached!")
 
 let load_keep i ((sp,kn),seg) =
   let mp = mp_of_kn kn in
-  let prefix = dir_of_sp sp, (mp,Dir_path.empty) in
+  let prefix = dir_of_sp sp, (mp,DirPath.empty) in
     begin
       try
 	let prefix',objects = MPmap.find mp !modtab_objects in
@@ -328,7 +328,7 @@ let load_keep i ((sp,kn),seg) =
 
 let open_keep i ((sp,kn),seg) =
   let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
-    open_objects i (dirpath,(mp,Dir_path.empty)) seg
+    open_objects i (dirpath,(mp,DirPath.empty)) seg
 
 let in_modkeep : lib_objects -> obj =
   declare_object {(default_object "MODULE KEEP OBJECTS") with
@@ -506,7 +506,7 @@ let rec get_modtype_substobjs env mp_from inline = function
 (* add objects associated to them *)
 let process_module_bindings argids args =
   let process_arg id (mbid,(mty,ann)) =
-    let dir = Dir_path.make [id] in
+    let dir = DirPath.make [id] in
     let mp = MPbound mbid in
     let (mbids,mp_from,objs) =
       get_modtype_substobjs (Global.env()) mp (inline_annot ann) mty in
@@ -539,7 +539,7 @@ let intern_args interp_modtype (idl,(arg,ann)) =
   let lib_dir = Lib.library_dp() in
   let mbids = List.map (fun (_,id) -> MBId.make lib_dir id) idl in
   let mty = interp_modtype (Global.env()) arg in
-  let dirs = List.map (fun (_,id) -> Dir_path.make [id]) idl in
+  let dirs = List.map (fun (_,id) -> DirPath.make [id]) idl in
   let (mbi,mp_from,objs) = get_modtype_substobjs (Global.env())
     (MPbound (List.hd mbids)) inl mty in
   List.map2
@@ -643,7 +643,7 @@ let module_objects mp =
 (************************************************************************)
 (* libraries *)
 
-type library_name = Dir_path.t
+type library_name = DirPath.t
 
 (* The first two will form substitutive_objects, the last one is keep *)
 type library_objects =
@@ -890,18 +890,18 @@ let lift_oname (sp,kn) =
 
 let cache_include (oname,(me,(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
-  let prefix = (dir,(mp1,Dir_path.empty)) in
+  let prefix = (dir,(mp1,DirPath.empty)) in
     load_objects 1 prefix objs;
     open_objects 1 prefix objs
 
 let load_include  i (oname,(me,(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
-  let prefix = (dir,(mp1,Dir_path.empty)) in
+  let prefix = (dir,(mp1,DirPath.empty)) in
     load_objects i prefix objs
 
 let open_include i (oname,(me,(mbis,mp1,objs))) =
   let dir,mp1 = lift_oname oname in
-  let prefix = (dir,(mp1,Dir_path.empty)) in
+  let prefix = (dir,(mp1,DirPath.empty)) in
     open_objects i prefix objs
 
 let subst_include (subst,(me,substobj)) =
diff --git a/library/declaremods.mli b/library/declaremods.mli
index f3c06b158..06446e2eb 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -104,7 +104,7 @@ val module_objects : module_path -> library_segment
 
 (** {6 Libraries i.e. modules on disk } *)
 
-type library_name = Dir_path.t
+type library_name = DirPath.t
 
 type library_objects
 
diff --git a/library/decls.ml b/library/decls.ml
index 35b75dab1..0ceea8b43 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -18,7 +18,7 @@ open Libnames
 (** Datas associated to section variables and local definitions *)
 
 type variable_data =
-    Dir_path.t * bool (* opacity *) * Univ.constraints * logical_kind
+    DirPath.t * bool (* opacity *) * Univ.constraints * logical_kind
 
 let vartab = ref (Id.Map.empty : variable_data Id.Map.t)
 
@@ -65,7 +65,7 @@ let initialize_named_context_for_proof () =
 let last_section_hyps dir =
   fold_named_context
     (fun (id,_,_) sec_ids ->
-      try if Dir_path.equal dir (variable_path id) then id::sec_ids else sec_ids
+      try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids
       with Not_found -> sec_ids)
     (Environ.named_context (Global.env()))
     ~init:[]
diff --git a/library/decls.mli b/library/decls.mli
index 2e080c7ba..87d963cd4 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -18,10 +18,10 @@ open Decl_kinds
 (** Registration and access to the table of variable *)
 
 type variable_data =
-    Dir_path.t * bool (** opacity *) * Univ.constraints * logical_kind
+    DirPath.t * bool (** opacity *) * Univ.constraints * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
-val variable_path : variable -> Dir_path.t
+val variable_path : variable -> DirPath.t
 val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
@@ -40,4 +40,4 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 (** Miscellaneous functions *)
 
-val last_section_hyps : Dir_path.t -> Id.t list
+val last_section_hyps : DirPath.t -> Id.t list
diff --git a/library/global.mli b/library/global.mli
index 141cfe50b..f8edf3165 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.t -> Id.t -> global_declaration -> constant
+  DirPath.t -> Id.t -> global_declaration -> constant
 val add_mind        :
-  Dir_path.t -> Id.t -> mutual_inductive_entry -> mutual_inductive
+  DirPath.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.t] argument to create a
+   Both [start_*] functions take the [DirPath.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.t -> bool
 
 (** Compiled modules *)
-val start_library : Dir_path.t -> module_path
-val export : Dir_path.t -> module_path * compiled_library * native_library
+val start_library : DirPath.t -> module_path
+val export : DirPath.t -> module_path * compiled_library * native_library
 val import : compiled_library -> Digest.t ->
   module_path * Nativecode.symbol array
 
diff --git a/library/globnames.ml b/library/globnames.ml
index 02570d339..50c91cc05 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -138,26 +138,26 @@ let constr_of_global_or_constr = function
 
 (** {6 Temporary function to brutally form kernel names from section paths } *)
 
-let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (Label.of_id id)
+let encode_mind dir id = make_mind (MPfile dir) DirPath.empty (Label.of_id id)
 
-let encode_con dir id = make_con (MPfile dir) Dir_path.empty (Label.of_id id)
+let encode_con dir id = make_con (MPfile dir) DirPath.empty (Label.of_id id)
 
 let check_empty_section dp =
-  if not (Dir_path.is_empty dp) then
+  if not (DirPath.is_empty dp) then
     anomaly (Pp.str "Section part should be empty!")
 
 let decode_mind kn =
   let rec dir_of_mp = function
-    | MPfile dir -> Dir_path.repr dir
+    | MPfile dir -> DirPath.repr dir
     | MPbound mbid ->
 	let _,_,dp = MBId.repr mbid in
 	let id = MBId.to_id mbid in
-	  id::(Dir_path.repr dp)
+	  id::(DirPath.repr dp)
     | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
   in
   let mp,sec_dir,l = repr_mind kn in
   check_empty_section sec_dir;
-  (Dir_path.make (dir_of_mp mp)),Label.to_id l
+  (DirPath.make (dir_of_mp mp)),Label.to_id l
 
 let decode_con kn =
   let mp,sec_dir,l = repr_con kn in
diff --git a/library/globnames.mli b/library/globnames.mli
index 1e53186f4..74da2cca8 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -83,10 +83,10 @@ val constr_of_global_or_constr : global_reference_or_constr -> constr
 
 (** {6 Temporary function to brutally form kernel names from section paths } *)
 
-val encode_mind : Dir_path.t -> Id.t -> mutual_inductive
-val decode_mind : mutual_inductive -> Dir_path.t * Id.t
-val encode_con : Dir_path.t -> Id.t -> constant
-val decode_con : constant -> Dir_path.t * Id.t
+val encode_mind : DirPath.t -> Id.t -> mutual_inductive
+val decode_mind : mutual_inductive -> DirPath.t * Id.t
+val encode_con : DirPath.t -> Id.t -> constant
+val decode_con : constant -> DirPath.t * Id.t
 
 (** {6 Popping one level of section in global names } *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 6b3110c20..baed92bd5 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -92,7 +92,7 @@ let segment_of_objects prefix =
    sections, but on the contrary there are many constructions of section
    paths based on the library path. *)
 
-let initial_prefix = default_library,(Names.initial_path,Names.Dir_path.empty)
+let initial_prefix = default_library,(Names.initial_path,Names.DirPath.empty)
 
 let lib_stk = ref ([] : library_segment)
 
@@ -106,10 +106,10 @@ let library_dp () =
 let path_prefix = ref initial_prefix
 
 let sections_depth () =
-  List.length (Names.Dir_path.repr (snd (snd !path_prefix)))
+  List.length (Names.DirPath.repr (snd (snd !path_prefix)))
 
 let sections_are_opened () =
-  match Names.Dir_path.repr (snd (snd !path_prefix)) with
+  match Names.DirPath.repr (snd (snd !path_prefix)) with
       [] -> false
     | _ -> true
 
@@ -127,10 +127,10 @@ let make_path id = Libnames.make_path (cwd ()) id
 let make_path_except_section id = Libnames.make_path (cwd_except_section ()) id
 
 let path_of_include () =
-  let dir = Names.Dir_path.repr (cwd ()) in
+  let dir = Names.DirPath.repr (cwd ()) in
   let new_dir = List.tl dir in
   let id = List.hd dir in
-    Libnames.make_path (Names.Dir_path.make new_dir) id
+    Libnames.make_path (Names.DirPath.make new_dir) id
 
 let current_prefix () = snd !path_prefix
 
@@ -275,7 +275,7 @@ let current_mod_id () =
 
 let start_mod is_type export id mp fs =
   let dir = add_dirpath_suffix (fst !path_prefix) id in
-  let prefix = dir,(mp,Names.Dir_path.empty) in
+  let prefix = dir,(mp,Names.DirPath.empty) in
   let sp = make_path id in
   let oname = sp, make_kn id in
   let exists =
@@ -328,9 +328,9 @@ let contents_after = function
 let start_compilation s mp =
   if !comp_name != None then
     error "compilation unit is already started";
-  if not (Names.Dir_path.equal (snd (snd (!path_prefix))) Names.Dir_path.empty) then
+  if not (Names.DirPath.equal (snd (snd (!path_prefix))) Names.DirPath.empty) then
     error "some sections are already opened";
-  let prefix = s, (mp, Names.Dir_path.empty) in
+  let prefix = s, (mp, Names.DirPath.empty) in
   let _ = add_anonymous_entry (CompilingLibrary prefix) in
   comp_name := Some s;
   path_prefix := prefix
@@ -356,7 +356,7 @@ let end_compilation dir =
     match !comp_name with
       | None -> anomaly (Pp.str "There should be a module name...")
       | Some m ->
-	  if not (Names.Dir_path.equal m dir) then anomaly
+	  if not (Names.DirPath.equal m dir) then anomaly
 	    (str "The current open module has name" ++ spc () ++ pr_dirpath m ++
              spc () ++ str "and not" ++ spc () ++ pr_dirpath m);
   in
@@ -621,7 +621,7 @@ let label_before_name (loc,id) =
 
 (* State and initialization. *)
 
-type frozen = Names.Dir_path.t option * library_segment
+type frozen = Names.DirPath.t option * library_segment
 
 let freeze () = (!comp_name, !lib_stk)
 
@@ -654,11 +654,11 @@ let rec dp_of_mp modp =
 
 let rec split_mp mp =
   match mp with
-    | Names.MPfile dp -> dp,  Names.Dir_path.empty
+    | Names.MPfile dp -> dp,  Names.DirPath.empty
     | Names.MPdot (prfx, lbl) ->
 	let mprec, dprec = split_mp prfx in
-	  mprec, Names.Dir_path.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.Dir_path.repr dprec))
-    | Names.MPbound mbid -> let (_, id, dp) = Names.MBId.repr mbid in  library_dp(), Names.Dir_path.make [id]
+	  mprec, Names.DirPath.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.DirPath.repr dprec))
+    | Names.MPbound mbid -> let (_, id, dp) = Names.MBId.repr mbid in  library_dp(), Names.DirPath.make [id]
 
 let split_modpath mp =
   let rec aux = function
@@ -695,13 +695,13 @@ let remove_section_part ref =
 
 let con_defined_in_sec kn =
   let _,dir,_ = Names.repr_con kn in
-  not (Names.Dir_path.is_empty dir) &&
-  Names.Dir_path.equal (fst (split_dirpath dir)) (snd (current_prefix ()))
+  not (Names.DirPath.is_empty dir) &&
+  Names.DirPath.equal (fst (split_dirpath dir)) (snd (current_prefix ()))
 
 let defined_in_sec kn =
   let _,dir,_ = Names.repr_mind kn in
-  not (Names.Dir_path.is_empty dir) &&
-  Names.Dir_path.equal (fst (split_dirpath dir)) (snd (current_prefix ()))
+  not (Names.DirPath.is_empty dir) &&
+  Names.DirPath.equal (fst (split_dirpath dir)) (snd (current_prefix ()))
 
 let discharge_global = function
   | ConstRef kn when con_defined_in_sec kn ->
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 } *)
 
diff --git a/library/libnames.ml b/library/libnames.ml
index 9f129793e..43ece3417 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -13,38 +13,38 @@ open Names
 
 (**********************************************)
 
-let pr_dirpath sl = (str (Dir_path.to_string sl))
+let pr_dirpath sl = (str (DirPath.to_string sl))
 
 (*s Operations on dirpaths *)
 
 (* Pop the last n module idents *)
 let pop_dirpath_n n dir =
-  Dir_path.make (List.skipn n (Dir_path.repr dir))
+  DirPath.make (List.skipn n (DirPath.repr dir))
 
-let pop_dirpath p = match Dir_path.repr p with
+let pop_dirpath p = match DirPath.repr p with
   | [] -> anomaly (str "dirpath_prefix: empty dirpath")
-  | _::l -> Dir_path.make l
+  | _::l -> DirPath.make l
 
 let is_dirpath_prefix_of d1 d2 =
-  List.prefix_of (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2))
+  List.prefix_of (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
 
 let chop_dirpath n d =
-  let d1,d2 = List.chop n (List.rev (Dir_path.repr d)) in
-    Dir_path.make (List.rev d1), Dir_path.make (List.rev d2)
+  let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in
+    DirPath.make (List.rev d1), DirPath.make (List.rev d2)
 
 let drop_dirpath_prefix d1 d2 =
-  let d = Util.List.drop_prefix (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2)) in
-    Dir_path.make (List.rev d)
+  let d = Util.List.drop_prefix (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) in
+    DirPath.make (List.rev d)
 
-let append_dirpath d1 d2 = Dir_path.make (Dir_path.repr d2 @ Dir_path.repr d1)
+let append_dirpath d1 d2 = DirPath.make (DirPath.repr d2 @ DirPath.repr d1)
 
 (* To know how qualified a name should be to be understood in the current env*)
-let add_dirpath_prefix id d = Dir_path.make (Dir_path.repr d @ [id])
+let add_dirpath_prefix id d = DirPath.make (DirPath.repr d @ [id])
 
 let split_dirpath d =
-  let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l)
+  let l = DirPath.repr d in (DirPath.make (List.tl l), List.hd l)
 
-let add_dirpath_suffix p id = Dir_path.make (id :: Dir_path.repr p)
+let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p)
 
 (* parsing *)
 let parse_dir s =
@@ -68,22 +68,22 @@ let dirpath_of_string s =
   | "" -> []
   | _ -> parse_dir s
   in
-  Dir_path.make path
+  DirPath.make path
 
-let string_of_dirpath = Names.Dir_path.to_string
+let string_of_dirpath = Names.DirPath.to_string
 
-module Dirset = Set.Make(struct type t = Dir_path.t let compare = Dir_path.compare end)
-module Dirmap = Map.Make(struct type t = Dir_path.t let compare = Dir_path.compare end)
+module Dirset = Set.Make(struct type t = DirPath.t let compare = DirPath.compare end)
+module Dirmap = Map.Make(struct type t = DirPath.t let compare = DirPath.compare end)
 
 (*s Section paths are absolute names *)
 
 type full_path = {
-  dirpath : Dir_path.t ;
+  dirpath : DirPath.t ;
   basename : Id.t }
 
 let eq_full_path p1 p2 =
   Id.equal p1.basename p2.basename &&
-  Dir_path.equal p1.dirpath p2.dirpath
+  DirPath.equal p1.dirpath p2.dirpath
 
 let make_path pa id = { dirpath = pa; basename = id }
 
@@ -92,9 +92,9 @@ let repr_path { dirpath = pa; basename = id } = (pa,id)
 (* parsing and printing of section paths *)
 let string_of_path sp =
   let (sl,id) = repr_path sp in
-  match Dir_path.repr sl with
+  match DirPath.repr sl with
   | [] -> Id.to_string id
-  | _ -> (Dir_path.to_string sl) ^ "." ^ (Id.to_string id)
+  | _ -> (DirPath.to_string sl) ^ "." ^ (Id.to_string id)
 
 let sp_ord sp1 sp2 =
   let (p1,id1) = repr_path sp1
@@ -124,8 +124,8 @@ let pr_path sp = str (string_of_path sp)
 
 let restrict_path n sp =
   let dir, s = repr_path sp in
-  let dir' = List.firstn n (Dir_path.repr dir) in
-  make_path (Dir_path.make dir') s
+  let dir' = List.firstn n (DirPath.repr dir) in
+  make_path (DirPath.make dir') s
 
 (*s qualified names *)
 type qualid = full_path
@@ -141,30 +141,30 @@ let pr_qualid = pr_path
 let qualid_of_string = path_of_string
 
 let qualid_of_path sp = sp
-let qualid_of_ident id = make_qualid Dir_path.empty id
+let qualid_of_ident id = make_qualid DirPath.empty id
 let qualid_of_dirpath dir =
   let (l,a) = split_dirpath dir in
   make_qualid l a
 
 type object_name = full_path * kernel_name
 
-type object_prefix = Dir_path.t * (module_path * Dir_path.t)
+type object_prefix = DirPath.t * (module_path * DirPath.t)
 
 let make_oname (dirpath,(mp,dir)) id =
   make_path dirpath id, make_kn mp dir (Label.of_id id)
 
-(* to this type are mapped Dir_path.t's in the nametab *)
+(* to this type are mapped DirPath.t's in the nametab *)
 type global_dir_reference =
   | DirOpenModule of object_prefix
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of Dir_path.t
+  | DirClosedSection of DirPath.t
       (* this won't last long I hope! *)
 
 let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) =
-  Dir_path.equal d1 d2 &&
-  Dir_path.equal p1 p2 &&
+  DirPath.equal d1 d2 &&
+  DirPath.equal p1 p2 &&
   mp_eq mp1 mp2
 
 let eq_global_dir_reference r1 r2 = match r1, r2 with
@@ -172,7 +172,7 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
 | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
 | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
 | DirModule op1, DirModule op2 -> eq_op op1 op2
-| DirClosedSection dp1, DirClosedSection dp2 -> Dir_path.equal dp1 dp2
+| DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2
 | _ -> false
 
 type reference =
diff --git a/library/libnames.mli b/library/libnames.mli
index 090709549..c44fea543 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -13,31 +13,31 @@ open Names
 (** {6 Dirpaths } *)
 (** FIXME: ought to be in Names.dir_path *)
 
-val pr_dirpath : Dir_path.t -> Pp.std_ppcmds
+val pr_dirpath : DirPath.t -> Pp.std_ppcmds
 
-val dirpath_of_string : string -> Dir_path.t
-val string_of_dirpath : Dir_path.t -> string
+val dirpath_of_string : string -> DirPath.t
+val string_of_dirpath : DirPath.t -> string
 
-(** Pop the suffix of a [Dir_path.t] *)
-val pop_dirpath : Dir_path.t -> Dir_path.t
+(** Pop the suffix of a [DirPath.t] *)
+val pop_dirpath : DirPath.t -> DirPath.t
 
 (** Pop the suffix n times *)
-val pop_dirpath_n : int -> Dir_path.t -> Dir_path.t
+val pop_dirpath_n : int -> DirPath.t -> DirPath.t
 
-(** Give the immediate prefix and basename of a [Dir_path.t] *)
-val split_dirpath : Dir_path.t -> Dir_path.t * Id.t
+(** Give the immediate prefix and basename of a [DirPath.t] *)
+val split_dirpath : DirPath.t -> DirPath.t * Id.t
 
-val add_dirpath_suffix : Dir_path.t -> module_ident -> Dir_path.t
-val add_dirpath_prefix : module_ident -> Dir_path.t -> Dir_path.t
+val add_dirpath_suffix : DirPath.t -> module_ident -> DirPath.t
+val add_dirpath_prefix : module_ident -> DirPath.t -> DirPath.t
 
-val chop_dirpath : int -> Dir_path.t -> Dir_path.t * Dir_path.t
-val append_dirpath : Dir_path.t -> Dir_path.t -> Dir_path.t
+val chop_dirpath : int -> DirPath.t -> DirPath.t * DirPath.t
+val append_dirpath : DirPath.t -> DirPath.t -> DirPath.t
 
-val drop_dirpath_prefix : Dir_path.t -> Dir_path.t -> Dir_path.t
-val is_dirpath_prefix_of : Dir_path.t -> Dir_path.t -> bool
+val drop_dirpath_prefix : DirPath.t -> DirPath.t -> DirPath.t
+val is_dirpath_prefix_of : DirPath.t -> DirPath.t -> bool
 
-module Dirset : Set.S with type elt = Dir_path.t
-module Dirmap : Map.S with type key = Dir_path.t
+module Dirset : Set.S with type elt = DirPath.t
+module Dirmap : Map.S with type key = DirPath.t
 
 (** {6 Full paths are {e absolute} paths of declarations } *)
 type full_path
@@ -45,11 +45,11 @@ type full_path
 val eq_full_path : full_path -> full_path -> bool
 
 (** Constructors of [full_path] *)
-val make_path : Dir_path.t -> Id.t -> full_path
+val make_path : DirPath.t -> Id.t -> full_path
 
 (** Destructors of [full_path] *)
-val repr_path : full_path -> Dir_path.t * Id.t
-val dirpath : full_path -> Dir_path.t
+val repr_path : full_path -> DirPath.t * Id.t
+val dirpath : full_path -> DirPath.t
 val basename : full_path -> Id.t
 
 (** Parsing and printing of section path as ["coq_root.module.id"] *)
@@ -69,8 +69,8 @@ val restrict_path : int -> full_path -> full_path
 
 type qualid
 
-val make_qualid : Dir_path.t -> Id.t -> qualid
-val repr_qualid : qualid -> Dir_path.t * Id.t
+val make_qualid : DirPath.t -> Id.t -> qualid
+val repr_qualid : qualid -> DirPath.t * Id.t
 
 val qualid_eq : qualid -> qualid -> bool
 
@@ -82,7 +82,7 @@ val qualid_of_string : string -> qualid
    qualified name denoting the same name *)
 
 val qualid_of_path : full_path -> qualid
-val qualid_of_dirpath : Dir_path.t -> qualid
+val qualid_of_dirpath : DirPath.t -> qualid
 val qualid_of_ident : Id.t -> qualid
 
 (** Both names are passed to objects: a "semantic" [kernel_name], which
@@ -91,19 +91,19 @@ val qualid_of_ident : Id.t -> qualid
 
 type object_name = full_path * kernel_name
 
-type object_prefix = Dir_path.t * (module_path * Dir_path.t)
+type object_prefix = DirPath.t * (module_path * DirPath.t)
 
 val eq_op : object_prefix -> object_prefix -> bool
 
 val make_oname : object_prefix -> Id.t -> object_name
 
-(** to this type are mapped [Dir_path.t]'s in the nametab *)
+(** to this type are mapped [DirPath.t]'s in the nametab *)
 type global_dir_reference =
   | DirOpenModule of object_prefix
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of Dir_path.t
+  | DirClosedSection of DirPath.t
       (** this won't last long I hope! *)
 
 val eq_global_dir_reference : 
diff --git a/library/library.ml b/library/library.ml
index 0fdd6d75e..92104348e 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -20,7 +20,7 @@ open Lib
 (*************************************************************************)
 (*s Load path. Mapping from physical to logical paths etc.*)
 
-type logical_path = Dir_path.t
+type logical_path = DirPath.t
 
 let load_paths = ref ([] : (CUnix.physical_path * logical_path * bool) list)
 
@@ -49,15 +49,15 @@ let add_load_path isroot (phys_path,coq_path) =
   let filter (p, _, _) = String.equal p phys_path in
     match List.filter filter !load_paths with
       | [_,dir,_] ->
-	  if not (Dir_path.equal coq_path dir)
+	  if not (DirPath.equal coq_path dir)
             (* If this is not the default -I . to coqtop *)
             && not
             (String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name)
-		&& Dir_path.equal coq_path (Nameops.default_root_prefix))
+		&& DirPath.equal coq_path (Nameops.default_root_prefix))
 	  then
 	    begin
               (* Assume the user is concerned by library naming *)
-	      if not (Dir_path.equal dir Nameops.default_root_prefix) then
+	      if not (DirPath.equal dir Nameops.default_root_prefix) then
 		Flags.if_warn msg_warning
 		  (str phys_path ++ strbrk " was previously bound to " ++
 		   pr_dirpath dir ++ strbrk "; it is remapped to " ++
@@ -71,7 +71,7 @@ let add_load_path isroot (phys_path,coq_path) =
 
 let extend_path_with_dirpath p dir =
   List.fold_left Filename.concat p
-    (List.rev_map Id.to_string (Dir_path.repr dir))
+    (List.rev_map Id.to_string (DirPath.repr dir))
 
 let root_paths_matching_dir_path dir =
   let rec aux = function
@@ -90,7 +90,7 @@ let root_paths_matching_dir_path dir =
 
 let intersections d1 d2 =
   let rec aux d1 =
-    if Dir_path.is_empty d1 then [d2] else
+    if DirPath.is_empty d1 then [d2] else
       let rest = aux (snd (chop_dirpath 1 d1)) in
       if is_dirpath_prefix_of d1 d2 then drop_dirpath_prefix d1 d2 :: rest
       else rest in
@@ -114,7 +114,7 @@ let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths
 (*s Modules on disk contain the following informations (after the magic
     number, and before the digest). *)
 
-type compilation_unit_name = Dir_path.t
+type compilation_unit_name = DirPath.t
 
 type library_disk = {
   md_name : compilation_unit_name;
@@ -134,7 +134,7 @@ type library_t = {
   library_imports : compilation_unit_name list;
   library_digest : Digest.t }
 
-module LibraryOrdered = Dir_path
+module LibraryOrdered = DirPath
 module LibraryMap = Map.Make(LibraryOrdered)
 module LibraryFilenameMap = Map.Make(LibraryOrdered)
 
@@ -182,7 +182,7 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (Dir_path.to_string dir))
+    error ("Unknown library " ^ (DirPath.to_string dir))
 
 let register_library_filename dir f =
   (* Not synchronized: overwrite the previous binding if one existed *)
@@ -205,7 +205,7 @@ let library_is_loaded dir =
   with Not_found -> false
 
 let library_is_opened dir =
-  List.exists (fun m -> Dir_path.equal m.library_name dir) !libraries_imports_list
+  List.exists (fun m -> DirPath.equal m.library_name dir) !libraries_imports_list
 
 let loaded_libraries () =
   List.map (fun m -> m.library_name) !libraries_loaded_list
@@ -226,7 +226,7 @@ let register_loaded_library m =
   in
   let rec aux = function
     | [] -> link m; [m]
-    | m'::_ as l when Dir_path.equal m'.library_name m.library_name -> l
+    | m'::_ as l when DirPath.equal m'.library_name m.library_name -> l
     | m'::l' -> m' :: aux l' in
   libraries_loaded_list := aux !libraries_loaded_list;
   libraries_table := LibraryMap.add m.library_name m !libraries_table
@@ -240,7 +240,7 @@ let register_loaded_library m =
 let rec remember_last_of_each l m =
   match l with
   | [] -> [m]
-  | m'::l' when Dir_path.equal m'.library_name m.library_name -> remember_last_of_each l' m
+  | m'::l' when DirPath.equal m'.library_name m.library_name -> remember_last_of_each l' m
   | m'::l' -> m' :: remember_last_of_each l' m
 
 let register_open_library export m =
@@ -254,7 +254,7 @@ let register_open_library export m =
 (* [open_library export explicit m] opens library [m] if not already
    opened _or_ if explicitly asked to be (re)opened *)
 
-let eq_lib_name m1 m2 = Dir_path.equal m1.library_name m2.library_name
+let eq_lib_name m1 m2 = DirPath.equal m1.library_name m2.library_name
 
 let open_library export explicit_libs m =
   if
@@ -303,7 +303,7 @@ let subst_import (_,o) = o
 let classify_import (_,export as obj) =
   if export then Substitute obj else Dispose
 
-let in_import : Dir_path.t * bool -> obj =
+let in_import : DirPath.t * bool -> obj =
   declare_object {(default_object "IMPORT LIBRARY") with
        cache_function = cache_import;
        open_function = open_import;
@@ -434,7 +434,7 @@ let rec intern_library needed (dir, f) =
   with Not_found ->
   (* [dir] is an absolute name which matches [f] which must be in loadpath *)
   let m = intern_from_file f in
-  if not (Dir_path.equal dir m.library_name) then
+  if not (DirPath.equal dir m.library_name) then
     errorlabstrm "load_physical_library"
       (str ("The file " ^ f ^ " contains library") ++ spc () ++
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
@@ -447,9 +447,9 @@ and intern_library_deps needed dir m =
 and intern_mandatory_library caller needed (dir,d) =
   let m,needed = intern_library needed (try_locate_absolute_library dir) in
   if not (String.equal d m.library_digest) then
-    errorlabstrm "" (strbrk ("Compiled library "^(Dir_path.to_string caller)^
+    errorlabstrm "" (strbrk ("Compiled library "^(DirPath.to_string caller)^
 	   ".vo makes inconsistent assumptions over library "
-	   ^(Dir_path.to_string dir)));
+	   ^(DirPath.to_string dir)));
   needed
 
 let rec_intern_library needed mref =
@@ -533,7 +533,7 @@ let discharge_require (_,o) = Some o
 
 (* open_function is never called from here because an Anticipate object *)
 
-type require_obj = library_t list * Dir_path.t list * bool option
+type require_obj = library_t list * DirPath.t list * bool option
 
 let in_require : require_obj -> obj =
   declare_object {(default_object "REQUIRE") with
@@ -604,11 +604,11 @@ let import_module export (loc,qid) =
 (*s Initializing the compilation of a library. *)
 
 let check_coq_overwriting p id =
-  let l = Dir_path.repr p in
+  let l = DirPath.repr p in
   let is_empty = match l with [] -> true | _ -> false in
   if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then
     errorlabstrm ""
-      (strbrk ("Cannot build module "^Dir_path.to_string p^"."^Id.to_string id^
+      (strbrk ("Cannot build module "^DirPath.to_string p^"."^Id.to_string id^
       ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
 
 let start_library f =
diff --git a/library/library.mli b/library/library.mli
index 6cf4107cb..11253087a 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -24,7 +24,7 @@ open Libobject
 (** Require = load in the environment + open (if the optional boolean
     is not [None]); mark also for export if the boolean is [Some true] *)
 val require_library : qualid located list -> bool option -> unit
-val require_library_from_dirpath : (Dir_path.t * string) list -> bool option -> unit
+val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit
 val require_library_from_file :
   Id.t option -> CUnix.physical_path -> bool option -> unit
 
@@ -34,40 +34,40 @@ val require_library_from_file :
 val import_module : bool -> qualid located -> unit
 
 (** {6 Start the compilation of a library } *)
-val start_library : string -> Dir_path.t * string
+val start_library : string -> DirPath.t * string
 
 (** {6 End the compilation of a library and save it to a ".vo" file } *)
-val save_library_to : Dir_path.t -> string -> unit
+val save_library_to : DirPath.t -> string -> unit
 
 (** {6 Interrogate the status of libraries } *)
 
   (** - Tell if a library is loaded or opened *)
-val library_is_loaded : Dir_path.t -> bool
-val library_is_opened : Dir_path.t -> bool
+val library_is_loaded : DirPath.t -> bool
+val library_is_opened : DirPath.t -> bool
 
   (** - Tell which libraries are loaded or imported *)
-val loaded_libraries : unit -> Dir_path.t list
-val opened_libraries : unit -> Dir_path.t list
+val loaded_libraries : unit -> DirPath.t list
+val opened_libraries : unit -> DirPath.t list
 
   (** - Return the full filename of a loaded library. *)
-val library_full_filename : Dir_path.t -> string
+val library_full_filename : DirPath.t -> string
 
   (** - Overwrite the filename of all libraries (used when restoring a state) *)
 val overwrite_library_filenames : string -> unit
 
 (** {6 Hook for the xml exportation of libraries } *)
-val set_xml_require : (Dir_path.t -> unit) -> unit
+val set_xml_require : (DirPath.t -> unit) -> unit
 
 (** {6 ... } *)
 (** Global load paths: a load path is a physical path in the file
-    system; to each load path is associated a Coq [Dir_path.t] (the "logical"
+    system; to each load path is associated a Coq [DirPath.t] (the "logical"
     path of the physical path) *)
 
 val get_load_paths : unit -> CUnix.physical_path list
-val get_full_load_paths : unit -> (CUnix.physical_path * Dir_path.t) list
-val add_load_path : bool -> CUnix.physical_path * Dir_path.t -> unit
+val get_full_load_paths : unit -> (CUnix.physical_path * DirPath.t) list
+val add_load_path : bool -> CUnix.physical_path * DirPath.t -> unit
 val remove_load_path : CUnix.physical_path -> unit
-val find_logical_path : CUnix.physical_path -> Dir_path.t
+val find_logical_path : CUnix.physical_path -> DirPath.t
 val is_in_load_paths : CUnix.physical_path -> bool
 
 (** {6 Locate a library in the load paths } *)
@@ -76,8 +76,8 @@ exception LibNotFound
 type library_location = LibLoaded | LibInPath
 
 val locate_qualified_library :
-  bool -> qualid -> library_location * Dir_path.t * CUnix.physical_path
-val try_locate_qualified_library : qualid located -> Dir_path.t * string
+  bool -> qualid -> library_location * DirPath.t * CUnix.physical_path
+val try_locate_qualified_library : qualid located -> DirPath.t * string
 
 (** {6 Statistics: display the memory use of a library. } *)
-val mem : Dir_path.t -> Pp.std_ppcmds
+val mem : DirPath.t -> Pp.std_ppcmds
diff --git a/library/nameops.ml b/library/nameops.ml
index 0891d306b..3b8de17d2 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -138,11 +138,11 @@ let name_fold_map f e = function
 
 let pr_lab l = str (Label.to_string l)
 
-let default_library = Names.Dir_path.initial (* = ["Top"] *)
+let default_library = Names.DirPath.initial (* = ["Top"] *)
 
 (*s Roots of the space of absolute names *)
 let coq_root = Id.of_string "Coq"
-let default_root_prefix = Dir_path.empty
+let default_root_prefix = DirPath.empty
 
 (* Metavariables *)
 let pr_meta = Pp.int
diff --git a/library/nameops.mli b/library/nameops.mli
index 1d3275d30..53cc86786 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -40,14 +40,14 @@ val pr_lab : Label.t -> Pp.std_ppcmds
 
 (** some preset paths *)
 
-val default_library : Dir_path.t
+val default_library : DirPath.t
 
 (** This is the root of the standard library of Coq *)
 val coq_root : module_ident
 
 (** This is the default root prefix for developments which doesn't
    mention a root *)
-val default_root_prefix : Dir_path.t
+val default_root_prefix : DirPath.t
 
 (** Metavariables *)
 val pr_meta : Term.metavariable -> Pp.std_ppcmds
diff --git a/library/nametab.ml b/library/nametab.ml
index 92b13d669..01324a3a4 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -42,7 +42,7 @@ type visibility = Until of int | Exactly of int
 (* Data structure for nametabs *******************************************)
 
 
-(* This module type will be instantiated by [full_path] of [Dir_path.t] *)
+(* This module type will be instantiated by [full_path] of [DirPath.t] *)
 (* The [repr] function is assumed to return the reversed list of idents. *)
 module type UserName = sig
   type t
@@ -194,7 +194,7 @@ let rec search tree = function
 
 let find_node qid tab =
   let (dir,id) = repr_qualid qid in
-    search (Id.Map.find id tab) (Dir_path.repr dir)
+    search (Id.Map.find id tab) (DirPath.repr dir)
 
 let locate qid tab =
   let o = match find_node qid tab with
@@ -238,7 +238,7 @@ let shortest_qualid ctx uname tab =
   in
   let ptab = Id.Map.find id tab in
   let found_dir = find_uname [] dir ptab in
-    make_qualid (Dir_path.make found_dir) id
+    make_qualid (DirPath.make found_dir) id
 
 let push_node node l =
   match node with
@@ -256,7 +256,7 @@ let rec search_prefixes tree = function
 let find_prefixes qid tab =
   try
     let (dir,id) = repr_qualid qid in
-    search_prefixes (Id.Map.find id tab) (Dir_path.repr dir)
+    search_prefixes (Id.Map.find id tab) (DirPath.repr dir)
   with Not_found -> []
 
 end
@@ -272,7 +272,7 @@ struct
   let to_string = string_of_path
   let repr sp =
     let dir,id = repr_path sp in
-      id, (Dir_path.repr dir)
+      id, (DirPath.repr dir)
 end
 
 module ExtRefEqual =
@@ -298,12 +298,10 @@ let the_tactictab = ref (KnTab.empty : kntab)
 type mptab = MPTab.t
 let the_modtypetab = ref (MPTab.empty : mptab)
 
-module DirPath =
+module DirPath' =
 struct
-  type t = Dir_path.t
-  let equal = Dir_path.equal
-  let to_string = Dir_path.to_string
-  let repr dir = match Dir_path.repr dir with
+  include DirPath
+  let repr dir = match DirPath.repr dir with
     | [] -> anomaly (Pp.str "Empty dirpath")
     | id :: l -> (id, l)
 end
@@ -314,7 +312,7 @@ struct
   let equal = eq_global_dir_reference
 end
 
-module DirTab = Make(DirPath)(GlobDir)
+module DirTab = Make(DirPath')(GlobDir)
 
 (* If we have a (closed) module M having a submodule N, than N does not
    have the entry in [the_dirtab]. *)
@@ -331,7 +329,7 @@ type globrevtab = full_path Globrevtab.t
 let the_globrevtab = ref (Globrevtab.empty : globrevtab)
 
 
-type mprevtab = Dir_path.t MPmap.t
+type mprevtab = DirPath.t MPmap.t
 let the_modrevtab = ref (MPmap.empty : mprevtab)
 
 type mptrevtab = full_path MPmap.t
@@ -479,7 +477,7 @@ let exists_modtype sp = MPTab.exists sp !the_modtypetab
 
 let path_of_global ref =
   match ref with
-    | VarRef id -> make_path Dir_path.empty id
+    | VarRef id -> make_path DirPath.empty id
     | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
 
 let dirpath_of_global ref =
@@ -501,7 +499,7 @@ let path_of_tactic kn =
 
 let shortest_qualid_of_global ctx ref =
   match ref with
-    | VarRef id -> make_qualid Dir_path.empty id
+    | VarRef id -> make_qualid DirPath.empty id
     | _ ->
         let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
         ExtRefTab.shortest_qualid ctx sp !the_ccitab
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 *)