Modulification of dir_path

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

19 files changed, 192 insertions, 191 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b5670a1a2..015fc9894 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 * section_variable_entry * logical_kind
+type variable_declaration = Dir_path.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 09bd6ac8b..54a0160bf 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 * section_variable_entry * logical_kind
+type variable_declaration = Dir_path.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 b58b355f7..10b04c588 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(initial_dir),[],None,[])
+  ref ((MPfile(Dir_path.initial),[],None,[])
 	 : module_path *  mod_bound_id 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(initial_dir),
+				       openmod_info := ((MPfile(Dir_path.initial),
 							 [],None,[]));
 				       library_cache := Dirmap.empty) }
 
 (* auxiliary functions to transform full_path and kernel_name given
-   by Lib into module_path and dir_path needed for modules *)
+   by Lib into module_path and Dir_path.t needed for modules *)
 
 let mp_of_kn kn =
   let mp,sec,l = repr_kn kn in
-    if dir_path_eq sec empty_dirpath then
+    if Dir_path.equal sec Dir_path.empty then
       MPdot (mp,l)
     else
       anomaly ("Non-empty section in module name!" ^ string_of_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,empty_dirpath)) in
-  let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
+  let prefix = (dir,(mp,Dir_path.empty)) in
+  let dirinfo = DirModule (dir,(mp,Dir_path.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,empty_dirpath)) in
-  let dirinfo = DirModule (dir,(mp,empty_dirpath)) in
+  let prefix = (dir,(mp,Dir_path.empty)) in
+  let dirinfo = DirModule (dir,(mp,Dir_path.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 "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,empty_dirpath) in
+  let prefix = dir_of_sp sp, (mp,Dir_path.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,empty_dirpath)) seg
+    open_objects i (dirpath,(mp,Dir_path.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 = make_dirpath [id] in
+    let dir = Dir_path.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) -> make_mbid lib_dir id) idl in
   let mty = interp_modtype (Global.env()) arg in
-  let dirs = List.map (fun (_,id) -> make_dirpath [id]) idl in
+  let dirs = List.map (fun (_,id) -> Dir_path.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
+type library_name = Dir_path.t
 
 (* The first two will form substitutive_objects, the last one is keep *)
 type library_objects =
@@ -885,18 +885,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,empty_dirpath)) in
+  let prefix = (dir,(mp1,Dir_path.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,empty_dirpath)) in
+  let prefix = (dir,(mp1,Dir_path.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,empty_dirpath)) in
+  let prefix = (dir,(mp1,Dir_path.empty)) in
     open_objects i prefix objs
 
 let subst_include (subst,(me,substobj)) =
diff --git a/library/declaremods.mli b/library/declaremods.mli
index e52e2620a..650b2cc81 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
+type library_name = Dir_path.t
 
 type library_objects
 
diff --git a/library/decls.ml b/library/decls.ml
index 205e51f9b..35b75dab1 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 * bool (* opacity *) * Univ.constraints * logical_kind
+    Dir_path.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_eq dir (variable_path id) then id::sec_ids else sec_ids
+      try if Dir_path.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 c424eacd3..2e080c7ba 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 * bool (** opacity *) * Univ.constraints * logical_kind
+    Dir_path.t * bool (** opacity *) * Univ.constraints * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
-val variable_path : variable -> dir_path
+val variable_path : variable -> Dir_path.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 -> Id.t list
+val last_section_hyps : Dir_path.t -> Id.t list
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 ... } *)
diff --git a/library/globnames.ml b/library/globnames.ml
index 9ce5451a1..efc46a7ac 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -138,28 +138,28 @@ 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) empty_dirpath (label_of_id id)
+let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (label_of_id id)
 
-let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
+let encode_con dir id = make_con (MPfile dir) Dir_path.empty (label_of_id id)
 
 let decode_mind kn =
   let rec dir_of_mp = function
-    | MPfile dir -> repr_dirpath dir
+    | MPfile dir -> Dir_path.repr dir
     | MPbound mbid ->
 	let _,_,dp = repr_mbid mbid in
 	let id = id_of_mbid mbid in
-	  id::(repr_dirpath dp)
+	  id::(Dir_path.repr dp)
     | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
   in
   let mp,sec_dir,l = repr_mind kn in
-    if (repr_dirpath sec_dir) = [] then
-     (make_dirpath (dir_of_mp mp)),id_of_label l
+    if (Dir_path.repr sec_dir) = [] then
+     (Dir_path.make (dir_of_mp mp)),id_of_label l
     else
       anomaly "Section part should be empty!"
 
 let decode_con kn =
   let mp,sec_dir,l = repr_con kn in
-    match mp,(repr_dirpath sec_dir) with
+    match mp,(Dir_path.repr sec_dir) with
 	MPfile dir,[] -> (dir,id_of_label l)
       | _ , [] -> anomaly "MPfile expected!"
       | _ -> anomaly "Section part should be empty!"
diff --git a/library/globnames.mli b/library/globnames.mli
index b82c68ea7..1e6f143cd 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -80,10 +80,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 -> Id.t -> mutual_inductive
-val decode_mind : mutual_inductive -> dir_path * Id.t
-val encode_con : dir_path -> Id.t -> constant
-val decode_con : constant -> dir_path * Id.t
+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
 
 (** {6 Popping one level of section in global names } *)
 
diff --git a/library/lib.ml b/library/lib.ml
index 6e82bfcb6..ed64b1f40 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.empty_dirpath)
+let initial_prefix = default_library,(Names.initial_path,Names.Dir_path.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.repr_dirpath (snd (snd !path_prefix)))
+  List.length (Names.Dir_path.repr (snd (snd !path_prefix)))
 
 let sections_are_opened () =
-  match Names.repr_dirpath (snd (snd !path_prefix)) with
+  match Names.Dir_path.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.repr_dirpath (cwd ()) in
+  let dir = Names.Dir_path.repr (cwd ()) in
   let new_dir = List.tl dir in
   let id = List.hd dir in
-    Libnames.make_path (Names.make_dirpath new_dir) id
+    Libnames.make_path (Names.Dir_path.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.empty_dirpath) in
+  let prefix = dir,(mp,Names.Dir_path.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_eq (snd (snd (!path_prefix))) Names.empty_dirpath) then
+  if not (Names.Dir_path.equal (snd (snd (!path_prefix))) Names.Dir_path.empty) then
     error "some sections are already opened";
-  let prefix = s, (mp, Names.empty_dirpath) in
+  let prefix = s, (mp, Names.Dir_path.empty) in
   let _ = add_anonymous_entry (CompilingLibrary prefix) in
   comp_name := Some s;
   path_prefix := prefix
@@ -356,9 +356,9 @@ let end_compilation dir =
     match !comp_name with
       | None -> anomaly "There should be a module name..."
       | Some m ->
-	  if not (Names.dir_path_eq m dir) then anomaly
-	    ("The current open module has name "^ (Names.string_of_dirpath m) ^
-	       " and not " ^ (Names.string_of_dirpath m));
+	  if not (Names.Dir_path.equal m dir) then anomaly
+	    ("The current open module has name "^ (Names.Dir_path.to_string m) ^
+	       " and not " ^ (Names.Dir_path.to_string m));
   in
   let (after,mark,before) = split_lib_at_opening oname in
   comp_name := None;
@@ -621,7 +621,7 @@ let label_before_name (loc,id) =
 
 (* State and initialization. *)
 
-type frozen = Names.dir_path option * library_segment
+type frozen = Names.Dir_path.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.empty_dirpath
+    | Names.MPfile dp -> dp,  Names.Dir_path.empty
     | Names.MPdot (prfx, lbl) ->
 	let mprec, dprec = split_mp prfx in
-	  mprec, Names.make_dirpath (Names.Id.of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
-    | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [id]
+	  mprec, Names.Dir_path.make (Names.Id.of_string (Names.string_of_label lbl) :: (Names.Dir_path.repr dprec))
+    | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.Dir_path.make [id]
 
 let split_modpath mp =
   let rec aux = function
@@ -703,13 +703,13 @@ let pop_con con =
 
 let con_defined_in_sec kn =
   let _,dir,_ = Names.repr_con kn in
-  not (Names.dir_path_eq dir Names.empty_dirpath) &&
-  Names.dir_path_eq (fst (split_dirpath dir)) (snd (current_prefix ()))
+  not (Names.Dir_path.equal dir Names.Dir_path.empty) &&
+  Names.Dir_path.equal (fst (split_dirpath dir)) (snd (current_prefix ()))
 
 let defined_in_sec kn =
   let _,dir,_ = Names.repr_mind kn in
-  not (Names.dir_path_eq dir Names.empty_dirpath) &&
-  Names.dir_path_eq (fst (split_dirpath dir)) (snd (current_prefix ()))
+  not (Names.Dir_path.equal dir Names.Dir_path.empty) &&
+  Names.Dir_path.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 75e18b194..13a79caf1 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
-val cwd_except_section : unit -> Names.dir_path
-val current_dirpath : bool -> Names.dir_path (* false = except sections *)
+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 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
+val current_prefix : unit -> Names.module_path * Names.Dir_path.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 -> Names.module_path -> unit
-val end_compilation : Names.dir_path -> Libnames.object_prefix * library_segment
+val start_compilation : Names.Dir_path.t -> Names.module_path -> unit
+val end_compilation : Names.Dir_path.t -> Libnames.object_prefix * library_segment
 
-(** The function [library_dp] returns the [dir_path] of the current
+(** The function [library_dp] returns the [Dir_path.t] of the current
    compiling library (or [default_library]) *)
-val library_dp : unit -> Names.dir_path
+val library_dp : unit -> Names.Dir_path.t
 
 (** Extract the library part of a name even if in a section *)
-val dp_of_mp : Names.module_path -> Names.dir_path
-val split_mp : Names.module_path -> Names.dir_path * Names.dir_path
-val split_modpath : Names.module_path -> Names.dir_path * Names.Id.t list
-val library_part :  Globnames.global_reference -> Names.dir_path
-val remove_section_part : Globnames.global_reference -> Names.dir_path
+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
 
 (** {6 Sections } *)
 
diff --git a/library/libnames.ml b/library/libnames.ml
index ee24b2575..8e026d8c2 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -13,38 +13,38 @@ open Names
 
 (**********************************************)
 
-let pr_dirpath sl = (str (string_of_dirpath sl))
+let pr_dirpath sl = (str (Dir_path.to_string sl))
 
 (*s Operations on dirpaths *)
 
 (* Pop the last n module idents *)
 let pop_dirpath_n n dir =
-  make_dirpath (List.skipn n (repr_dirpath dir))
+  Dir_path.make (List.skipn n (Dir_path.repr dir))
 
-let pop_dirpath p = match repr_dirpath p with
+let pop_dirpath p = match Dir_path.repr p with
   | [] -> anomaly "dirpath_prefix: empty dirpath"
-  | _::l -> make_dirpath l
+  | _::l -> Dir_path.make l
 
 let is_dirpath_prefix_of d1 d2 =
-  List.prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+  List.prefix_of (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2))
 
 let chop_dirpath n d =
-  let d1,d2 = List.chop n (List.rev (repr_dirpath d)) in
-    make_dirpath (List.rev d1), make_dirpath (List.rev d2)
+  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 drop_dirpath_prefix d1 d2 =
-  let d = Util.List.drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in
-    make_dirpath (List.rev d)
+  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 append_dirpath d1 d2 = make_dirpath (repr_dirpath d2 @ repr_dirpath d1)
+let append_dirpath d1 d2 = Dir_path.make (Dir_path.repr d2 @ Dir_path.repr d1)
 
 (* To know how qualified a name should be to be understood in the current env*)
-let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
+let add_dirpath_prefix id d = Dir_path.make (Dir_path.repr d @ [id])
 
 let split_dirpath d =
-  let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
+  let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l)
 
-let add_dirpath_suffix p id = make_dirpath (id :: repr_dirpath p)
+let add_dirpath_suffix p id = Dir_path.make (id :: Dir_path.repr p)
 
 (* parsing *)
 let parse_dir s =
@@ -68,23 +68,22 @@ let dirpath_of_string s =
   | "" -> []
   | _ -> parse_dir s
   in
-  make_dirpath path
+  Dir_path.make path
 
-let string_of_dirpath = Names.string_of_dirpath
+let string_of_dirpath = Names.Dir_path.to_string
 
-
-module Dirset = Set.Make(struct type t = dir_path let compare = dir_path_ord end)
-module Dirmap = Map.Make(struct type t = dir_path let compare = dir_path_ord end)
+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)
 
 (*s Section paths are absolute names *)
 
 type full_path = {
-  dirpath : dir_path ;
+  dirpath : Dir_path.t ;
   basename : Id.t }
 
 let eq_full_path p1 p2 =
   Id.equal p1.basename p2.basename &&
-  Int.equal (dir_path_ord p1.dirpath p2.dirpath) 0
+  Int.equal (Dir_path.compare p1.dirpath p2.dirpath) 0
 
 let make_path pa id = { dirpath = pa; basename = id }
 
@@ -93,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 repr_dirpath sl with
+  match Dir_path.repr sl with
   | [] -> Id.to_string id
-  | _ -> (string_of_dirpath sl) ^ "." ^ (Id.to_string id)
+  | _ -> (Dir_path.to_string sl) ^ "." ^ (Id.to_string id)
 
 let sp_ord sp1 sp2 =
   let (p1,id1) = repr_path sp1
@@ -125,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 (repr_dirpath dir) in
-  make_path (make_dirpath dir') s
+  let dir' = List.firstn n (Dir_path.repr dir) in
+  make_path (Dir_path.make dir') s
 
 (*s qualified names *)
 type qualid = full_path
@@ -142,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 empty_dirpath id
+let qualid_of_ident id = make_qualid Dir_path.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 * (module_path * dir_path)
+type object_prefix = Dir_path.t * (module_path * Dir_path.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's in the nametab *)
+(* to this type are mapped Dir_path.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
+  | DirClosedSection of Dir_path.t
       (* this won't last long I hope! *)
 
 let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) =
-  Int.equal (dir_path_ord d1 d2) 0 &&
-  Int.equal (dir_path_ord p1 p2) 0 &&
+  Int.equal (Dir_path.compare d1 d2) 0 &&
+  Int.equal (Dir_path.compare p1 p2) 0 &&
   mp_eq mp1 mp2
 
 let eq_global_dir_reference r1 r2 = match r1, r2 with
@@ -173,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 -> Int.equal (dir_path_ord dp1 dp2) 0
+| DirClosedSection dp1, DirClosedSection dp2 -> Int.equal (Dir_path.compare dp1 dp2) 0
 | _ -> false
 
 type reference =
diff --git a/library/libnames.mli b/library/libnames.mli
index 08330349e..090709549 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -11,31 +11,33 @@ open Loc
 open Names
 
 (** {6 Dirpaths } *)
-val pr_dirpath : dir_path -> Pp.std_ppcmds
+(** FIXME: ought to be in Names.dir_path *)
 
-val dirpath_of_string : string -> dir_path
-val string_of_dirpath : dir_path -> string
+val pr_dirpath : Dir_path.t -> Pp.std_ppcmds
 
-(** Pop the suffix of a [dir_path] *)
-val pop_dirpath : dir_path -> dir_path
+val dirpath_of_string : string -> Dir_path.t
+val string_of_dirpath : Dir_path.t -> string
+
+(** Pop the suffix of a [Dir_path.t] *)
+val pop_dirpath : Dir_path.t -> Dir_path.t
 
 (** Pop the suffix n times *)
-val pop_dirpath_n : int -> dir_path -> dir_path
+val pop_dirpath_n : int -> Dir_path.t -> Dir_path.t
 
-(** Give the immediate prefix and basename of a [dir_path] *)
-val split_dirpath : dir_path -> dir_path * Id.t
+(** Give the immediate prefix and basename of a [Dir_path.t] *)
+val split_dirpath : Dir_path.t -> Dir_path.t * Id.t
 
-val add_dirpath_suffix : dir_path -> module_ident -> dir_path
-val add_dirpath_prefix : module_ident -> dir_path -> dir_path
+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 chop_dirpath : int -> dir_path -> dir_path * dir_path
-val append_dirpath : dir_path -> dir_path -> dir_path
+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 drop_dirpath_prefix : dir_path -> dir_path -> dir_path
-val is_dirpath_prefix_of : dir_path -> dir_path -> bool
+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
 
-module Dirset : Set.S with type elt = dir_path
-module Dirmap : Map.S with type key = dir_path
+module Dirset : Set.S with type elt = Dir_path.t
+module Dirmap : Map.S with type key = Dir_path.t
 
 (** {6 Full paths are {e absolute} paths of declarations } *)
 type full_path
@@ -43,11 +45,11 @@ type full_path
 val eq_full_path : full_path -> full_path -> bool
 
 (** Constructors of [full_path] *)
-val make_path : dir_path -> Id.t -> full_path
+val make_path : Dir_path.t -> Id.t -> full_path
 
 (** Destructors of [full_path] *)
-val repr_path : full_path -> dir_path * Id.t
-val dirpath : full_path -> dir_path
+val repr_path : full_path -> Dir_path.t * Id.t
+val dirpath : full_path -> Dir_path.t
 val basename : full_path -> Id.t
 
 (** Parsing and printing of section path as ["coq_root.module.id"] *)
@@ -67,8 +69,8 @@ val restrict_path : int -> full_path -> full_path
 
 type qualid
 
-val make_qualid : dir_path -> Id.t -> qualid
-val repr_qualid : qualid -> dir_path * Id.t
+val make_qualid : Dir_path.t -> Id.t -> qualid
+val repr_qualid : qualid -> Dir_path.t * Id.t
 
 val qualid_eq : qualid -> qualid -> bool
 
@@ -80,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 -> qualid
+val qualid_of_dirpath : Dir_path.t -> qualid
 val qualid_of_ident : Id.t -> qualid
 
 (** Both names are passed to objects: a "semantic" [kernel_name], which
@@ -89,19 +91,19 @@ val qualid_of_ident : Id.t -> qualid
 
 type object_name = full_path * kernel_name
 
-type object_prefix = dir_path * (module_path * dir_path)
+type object_prefix = Dir_path.t * (module_path * Dir_path.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]'s in the nametab *)
+(** to this type are mapped [Dir_path.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
+  | DirClosedSection of Dir_path.t
       (** this won't last long I hope! *)
 
 val eq_global_dir_reference : 
diff --git a/library/library.ml b/library/library.ml
index b25b1d313..e2b74c668 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
+type logical_path = Dir_path.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_eq coq_path dir)
+	  if not (Dir_path.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_eq coq_path (Nameops.default_root_prefix))
+		&& Dir_path.equal coq_path (Nameops.default_root_prefix))
 	  then
 	    begin
               (* Assume the user is concerned by library naming *)
-	      if not (dir_path_eq dir Nameops.default_root_prefix) then
+	      if not (Dir_path.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.map Id.to_string (List.rev (repr_dirpath dir)))
+    (List.map Id.to_string (List.rev (Dir_path.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_eq d1 empty_dirpath then [d2] else
+    if Dir_path.equal d1 Dir_path.empty 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
+type compilation_unit_name = Dir_path.t
 
 type library_disk = {
   md_name : compilation_unit_name;
@@ -136,8 +136,8 @@ type library_t = {
 
 module LibraryOrdered =
   struct
-    type t = dir_path
-    let compare = dir_path_ord
+    type t = Dir_path.t
+    let compare = Dir_path.compare
   end
 
 module LibraryMap = Map.Make(LibraryOrdered)
@@ -187,7 +187,7 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (string_of_dirpath dir))
+    error ("Unknown library " ^ (Dir_path.to_string dir))
 
 let register_library_filename dir f =
   (* Not synchronized: overwrite the previous binding if one existed *)
@@ -210,7 +210,7 @@ let library_is_loaded dir =
   with Not_found -> false
 
 let library_is_opened dir =
-  List.exists (fun m -> dir_path_eq m.library_name dir) !libraries_imports_list
+  List.exists (fun m -> Dir_path.equal m.library_name dir) !libraries_imports_list
 
 let loaded_libraries () =
   List.map (fun m -> m.library_name) !libraries_loaded_list
@@ -224,7 +224,7 @@ let opened_libraries () =
 let register_loaded_library m =
   let rec aux = function
     | [] -> [m]
-    | m'::_ as l when dir_path_eq m'.library_name m.library_name -> l
+    | m'::_ as l when Dir_path.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
@@ -238,7 +238,7 @@ let register_loaded_library m =
 let rec remember_last_of_each l m =
   match l with
   | [] -> [m]
-  | m'::l' when dir_path_eq m'.library_name m.library_name -> remember_last_of_each l' m
+  | m'::l' when Dir_path.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 =
@@ -252,7 +252,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_eq m1.library_name m2.library_name
+let eq_lib_name m1 m2 = Dir_path.equal m1.library_name m2.library_name
 
 let open_library export explicit_libs m =
   if
@@ -301,7 +301,7 @@ let subst_import (_,o) = o
 let classify_import (_,export as obj) =
   if export then Substitute obj else Dispose
 
-let in_import : dir_path * bool -> obj =
+let in_import : Dir_path.t * bool -> obj =
   declare_object {(default_object "IMPORT LIBRARY") with
        cache_function = cache_import;
        open_function = open_import;
@@ -428,7 +428,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_eq dir m.library_name) then
+  if not (Dir_path.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" ++
@@ -441,9 +441,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 "^(string_of_dirpath caller)^
+    errorlabstrm "" (strbrk ("Compiled library "^(Dir_path.to_string caller)^
 	   ".vo makes inconsistent assumptions over library "
-	   ^(string_of_dirpath dir)));
+	   ^(Dir_path.to_string dir)));
   needed
 
 let rec_intern_library needed mref =
@@ -525,7 +525,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 list * bool option
+type require_obj = library_t list * Dir_path.t list * bool option
 
 let in_require : require_obj -> obj =
   declare_object {(default_object "REQUIRE") with
@@ -596,11 +596,11 @@ let import_module export (loc,qid) =
 (*s Initializing the compilation of a library. *)
 
 let check_coq_overwriting p id =
-  let l = repr_dirpath p in
+  let l = Dir_path.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 "^string_of_dirpath p^"."^Id.to_string id^
+      (strbrk ("Cannot build module "^Dir_path.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 4e88a85b5..6cf4107cb 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 * string) list -> bool option -> unit
+val require_library_from_dirpath : (Dir_path.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 * string
+val start_library : string -> Dir_path.t * string
 
 (** {6 End the compilation of a library and save it to a ".vo" file } *)
-val save_library_to : dir_path -> string -> unit
+val save_library_to : Dir_path.t -> string -> unit
 
 (** {6 Interrogate the status of libraries } *)
 
   (** - Tell if a library is loaded or opened *)
-val library_is_loaded : dir_path -> bool
-val library_is_opened : dir_path -> bool
+val library_is_loaded : Dir_path.t -> bool
+val library_is_opened : Dir_path.t -> bool
 
   (** - Tell which libraries are loaded or imported *)
-val loaded_libraries : unit -> dir_path list
-val opened_libraries : unit -> dir_path list
+val loaded_libraries : unit -> Dir_path.t list
+val opened_libraries : unit -> Dir_path.t list
 
   (** - Return the full filename of a loaded library. *)
-val library_full_filename : dir_path -> string
+val library_full_filename : Dir_path.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 -> unit) -> unit
+val set_xml_require : (Dir_path.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] (the "logical"
+    system; to each load path is associated a Coq [Dir_path.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) list
-val add_load_path : bool -> CUnix.physical_path * dir_path -> unit
+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 remove_load_path : CUnix.physical_path -> unit
-val find_logical_path : CUnix.physical_path -> dir_path
+val find_logical_path : CUnix.physical_path -> Dir_path.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 * CUnix.physical_path
-val try_locate_qualified_library : qualid located -> dir_path * string
+  bool -> qualid -> library_location * Dir_path.t * CUnix.physical_path
+val try_locate_qualified_library : qualid located -> Dir_path.t * string
 
 (** {6 Statistics: display the memory use of a library. } *)
-val mem : dir_path -> Pp.std_ppcmds
+val mem : Dir_path.t -> Pp.std_ppcmds
diff --git a/library/nameops.ml b/library/nameops.ml
index f8f95135f..361a53d6b 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 (string_of_label l)
 
-let default_library = Names.initial_dir (* = ["Top"] *)
+let default_library = Names.Dir_path.initial (* = ["Top"] *)
 
 (*s Roots of the space of absolute names *)
 let coq_root = Id.of_string "Coq"
-let default_root_prefix = make_dirpath []
+let default_root_prefix = Dir_path.make []
 
 (* Metavariables *)
 let pr_meta = Pp.int
diff --git a/library/nameops.mli b/library/nameops.mli
index 3bdd64f75..6e9bde839 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -40,14 +40,14 @@ val pr_lab : label -> Pp.std_ppcmds
 
 (** some preset paths *)
 
-val default_library : dir_path
+val default_library : Dir_path.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
+val default_root_prefix : Dir_path.t
 
 (** Metavariables *)
 val pr_meta : Term.metavariable -> Pp.std_ppcmds
diff --git a/library/nametab.ml b/library/nametab.ml
index bbcee8b66..46d8dcc3f 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] *)
+(* This module type will be instantiated by [full_path] of [Dir_path.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) (repr_dirpath dir)
+    search (Id.Map.find id tab) (Dir_path.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 (make_dirpath found_dir) id
+    make_qualid (Dir_path.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) (repr_dirpath dir)
+    search_prefixes (Id.Map.find id tab) (Dir_path.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, (repr_dirpath dir)
+      id, (Dir_path.repr dir)
 end
 
 module ExtRefEqual =
@@ -308,10 +308,10 @@ let the_modtypetab = ref (MPTab.empty : mptab)
 
 module DirPath =
 struct
-  type t = dir_path
-  let equal d1 d2 = Int.equal (dir_path_ord d1 d2) 0
-  let to_string = string_of_dirpath
-  let repr dir = match repr_dirpath dir with
+  type t = Dir_path.t
+  let equal d1 d2 = Int.equal (Dir_path.compare d1 d2) 0
+  let to_string = Dir_path.to_string
+  let repr dir = match Dir_path.repr dir with
     | [] -> anomaly "Empty dirpath"
     | id :: l -> (id, l)
 end
@@ -339,7 +339,7 @@ type globrevtab = full_path Globrevtab.t
 let the_globrevtab = ref (Globrevtab.empty : globrevtab)
 
 
-type mprevtab = dir_path MPmap.t
+type mprevtab = Dir_path.t MPmap.t
 let the_modrevtab = ref (MPmap.empty : mprevtab)
 
 type mptrevtab = full_path MPmap.t
@@ -487,7 +487,7 @@ let exists_modtype sp = MPTab.exists sp !the_modtypetab
 
 let path_of_global ref =
   match ref with
-    | VarRef id -> make_path empty_dirpath id
+    | VarRef id -> make_path Dir_path.empty id
     | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab
 
 let dirpath_of_global ref =
@@ -509,7 +509,7 @@ let path_of_tactic kn =
 
 let shortest_qualid_of_global ctx ref =
   match ref with
-    | VarRef id -> make_qualid empty_dirpath id
+    | VarRef id -> make_qualid Dir_path.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 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 *)