Modulification of dir_path

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

92 files changed, 545 insertions, 479 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 31f75f4f9..49fe6d0ba 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -11,19 +11,19 @@ open Errors
 open Util
 open Names
 
-let pr_dirpath dp = str (string_of_dirpath dp)
-let default_root_prefix = make_dirpath []
+let pr_dirpath dp = str (Dir_path.to_string dp)
+let default_root_prefix = Dir_path.make []
 let split_dirpath d =
-  let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
-let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
+  let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l)
+let extend_dirpath p id = Dir_path.make (id :: Dir_path.repr p)
 
 type section_path = {
   dirpath : string list ;
   basename : string }
 let dir_of_path p =
-  make_dirpath (List.map Id.of_string p.dirpath)
+  Dir_path.make (List.map Id.of_string p.dirpath)
 let path_of_dirpath dir =
-  match repr_dirpath dir with
+  match Dir_path.repr dir with
       [] -> failwith "path_of_dirpath"
     | l::dir ->
         {dirpath=List.map Id.to_string dir;basename=Id.to_string l}
@@ -36,7 +36,7 @@ let pr_path sp =
 
 type library_objects
 
-type compilation_unit_name = dir_path
+type compilation_unit_name = Dir_path.t
 
 type library_disk = {
   md_name : compilation_unit_name;
@@ -61,10 +61,10 @@ type library_t = {
 
 module LibraryOrdered =
   struct
-    type t = dir_path
+    type t = Dir_path.t
     let compare d1 d2 =
       Pervasives.compare
-        (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+        (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2))
   end
 
 module LibrarySet = Set.Make(LibraryOrdered)
@@ -81,7 +81,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 library_full_filename dir = (find_library dir).library_filename
 
@@ -113,7 +113,7 @@ let check_one_lib admit (dir,m) =
 (*************************************************************************)
 (*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 list * logical_path list)
 
diff --git a/checker/checker.ml b/checker/checker.ml
index 5a7efacf8..1b7af5178 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -36,7 +36,7 @@ let parse_dir s =
 let dirpath_of_string s =
   match parse_dir s with
       [] -> Check.default_root_prefix
-    | dir -> make_dirpath (List.map Id.of_string dir)
+    | dir -> Dir_path.make (List.map Id.of_string dir)
 let path_of_string s =
   match parse_dir s with
       [] -> invalid_arg "path_of_string"
@@ -77,11 +77,11 @@ let convert_string d =
 let add_rec_path ~unix_path ~coq_root =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
-    let prefix = repr_dirpath coq_root in
+    let prefix = Dir_path.repr coq_root in
     let convert_dirs (lp, cp) =
       try
         let path = List.map convert_string (List.rev cp) @ prefix in
-        Some (lp, Names.make_dirpath path)
+        Some (lp, Names.Dir_path.make path)
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
@@ -113,9 +113,9 @@ let init_load_path () =
   let plugins = coqlib/"plugins" in
   (* NOTE: These directories are searched from last to first *)
   (* first standard library *)
-  add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.make_dirpath[coq_root]);
+  add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.Dir_path.make[coq_root]);
   (* then plugins *)
-  add_rec_path ~unix_path:plugins ~coq_root:(Names.make_dirpath [coq_root]);
+  add_rec_path ~unix_path:plugins ~coq_root:(Names.Dir_path.make [coq_root]);
   (* then user-contrib *)
   if Sys.file_exists user_contrib then
     add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
diff --git a/checker/environ.mli b/checker/environ.mli
index 36b76960f..0ec14cc92 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -27,8 +27,8 @@ val engagement : env -> Declarations.engagement option
 val set_engagement : Declarations.engagement -> env -> env
 
 (* Digests *)
-val add_digest : env -> dir_path -> Digest.t -> env
-val lookup_digest : env -> dir_path -> Digest.t
+val add_digest : env -> Dir_path.t -> Digest.t -> env
+val lookup_digest : env -> Dir_path.t -> Digest.t
 
 (* de Bruijn variables *)
 val rel_context : env -> rel_context
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index edd970f6b..548dd32fc 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -19,12 +19,12 @@ open Declarations
 open Environ
 
 let rec debug_string_of_mp = function
-  | MPfile sl -> string_of_dirpath sl
+  | MPfile sl -> Dir_path.to_string sl
   | MPbound uid -> "bound("^string_of_mbid uid^")"
   | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ string_of_label l
 
 let rec string_of_mp = function
-  | MPfile sl -> string_of_dirpath sl
+  | MPfile sl -> Dir_path.to_string sl
   | MPbound uid -> string_of_mbid uid
   | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7dfa29e16..b8e5fa043 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -253,10 +253,10 @@ and check_module env mp mb =
 
 and check_structure_field env mp lab res = function
   | SFBconst cb ->
-      let c = make_con mp empty_dirpath lab in
+      let c = make_con mp Dir_path.empty lab in
 	check_constant_declaration env c cb
   | SFBmind mib ->
-      let kn = make_mind mp empty_dirpath lab in
+      let kn = make_mind mp Dir_path.empty lab in
       let kn = mind_of_delta res kn in
 	Indtypes.check_inductive env kn mib
   | SFBmodule msb ->
diff --git a/checker/modops.ml b/checker/modops.ml
index 1c4a2916e..4330eff30 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -67,7 +67,7 @@ let module_body_of_type mp mtb =
 
 let rec add_signature mp sign resolver env = 
   let add_one env (l,elem) =
-    let kn = make_kn mp empty_dirpath l in
+    let kn = make_kn mp Dir_path.empty l in
     let con = constant_of_kn kn in
     let mind = mind_of_delta resolver (mind_of_kn kn) in
       match elem with
@@ -97,7 +97,7 @@ let strengthen_const mp_from l cb resolver =
   match cb.const_body with
     | Def _ -> cb
     | _ ->
-      let con = make_con mp_from empty_dirpath l in
+      let con = make_con mp_from Dir_path.empty l in
       (* let con =  constant_of_delta resolver con in*)
       { cb with const_body = Def (Declarations.from_val (Const con)) }
 
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index e5e4768a8..f0bcb3a12 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -43,9 +43,9 @@ let check_engagement env c =
 
 let report_clash f caller dir =
   let msg =
-    str "compiled library " ++ str(string_of_dirpath caller) ++
+    str "compiled library " ++ str(Dir_path.to_string caller) ++
     spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++
-    str(string_of_dirpath dir) ++ fnl() in
+    str(Dir_path.to_string dir) ++ fnl() in
   f msg
 
 
@@ -55,15 +55,15 @@ let check_imports f caller env needed =
       let actual_stamp = lookup_digest env dp in
       if stamp <> actual_stamp then report_clash f caller dp
     with Not_found ->
-      error ("Reference to unknown module " ^ (string_of_dirpath dp))
+      error ("Reference to unknown module " ^ (Dir_path.to_string dp))
   in
   List.iter check needed
 
 
 type compiled_library =
-    dir_path *
+    Dir_path.t *
     module_body *
-    (dir_path * Digest.t) list *
+    (Dir_path.t * Digest.t) list *
     engagement option
 
  (* Store the body of modules' opaque constants inside a table.  
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 390c2b9e7..951bed6c1 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -35,7 +35,7 @@ type namedmodule =
    constructors *)
 
 let add_mib_nameobjects mp l mib map =
-  let ind = make_mind mp empty_dirpath l in
+  let ind = make_mind mp Dir_path.empty l in
   let add_mip_nameobjects j oib map =
     let ip = (ind,j) in
     let map =
@@ -83,7 +83,7 @@ let check_conv_error error f env a1 a2 =
 
 (* for now we do not allow reorderings *)
 let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2= 
-  let kn = make_mind  mp1 empty_dirpath l in
+  let kn = make_mind  mp1 Dir_path.empty l in
   let error () = error_not_match l spec2 in
   let check_conv f = check_conv_error error f in
   let mib1 =
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 186ab170e..7163f4429 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -321,7 +321,7 @@ let print_pure_constr csr =
   and sp_display sp =
 (*    let dir,l = decode_kn sp in
     let ls =
-      match List.rev (List.map Id.to_string (repr_dirpath dir)) with
+      match List.rev (List.map Id.to_string (Dir_path.repr dir)) with
           ("Top"::l)-> l
 	| ("Coq"::_::l) -> l
 	| l             -> l
@@ -330,7 +330,7 @@ let print_pure_constr csr =
   and sp_con_display sp =
 (*    let dir,l = decode_kn sp in
     let ls =
-      match List.rev (List.map Id.to_string (repr_dirpath dir)) with
+      match List.rev (List.map Id.to_string (Dir_path.repr dir)) with
           ("Top"::l)-> l
 	| ("Coq"::_::l) -> l
 	| l             -> l
@@ -448,10 +448,10 @@ let encode_path loc prefix mpdir suffix id =
   let dir = match mpdir with
     | None -> []
     | Some (mp,dir) ->
-	(repr_dirpath (dirpath_of_string (string_of_mp mp))@
-	repr_dirpath dir) in
+	(Dir_path.repr (dirpath_of_string (string_of_mp mp))@
+	Dir_path.repr dir) in
   Qualid (loc, make_qualid
-    (make_dirpath (List.rev (Id.of_string prefix::dir@suffix))) id)
+    (Dir_path.make (List.rev (Id.of_string prefix::dir@suffix))) id)
 
 let raw_string_of_ref loc = function
   | ConstRef cst ->
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index e879f2fff..738c3e1f1 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -33,8 +33,8 @@ let mlexpr_of_name = function
       <:expr< Names.Name (Names.Id.of_string $str:Names.Id.to_string id$) >>
 
 let mlexpr_of_dirpath dir =
-  let l = Names.repr_dirpath dir in
-  <:expr< Names.make_dirpath $mlexpr_of_list mlexpr_of_ident l$ >>
+  let l = Names.Dir_path.repr dir in
+  <:expr< Names.Dir_path.make $mlexpr_of_list mlexpr_of_ident l$ >>
 
 let mlexpr_of_qualid qid =
   let (dir, id) = Libnames.repr_qualid qid in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 6cb97fd60..0e4d0c651 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -171,7 +171,7 @@ val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -
 val is_global : Id.t -> bool
 val construct_reference : named_context -> Id.t -> constr
 val global_reference : Id.t -> constr
-val global_reference_in_absolute_module : dir_path -> Id.t -> constr
+val global_reference_in_absolute_module : Dir_path.t -> Id.t -> constr
 
 (** Interprets a term as the left-hand side of a notation; the boolean
     list is a set and this set is [true] for a variable occurring in
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 4b2ca2004..a047a762b 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -21,7 +21,7 @@ open Smartlocate
 
 type message = string
 
-let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
 
 let find_reference locstr dir s =
   let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
@@ -64,10 +64,10 @@ let gen_constant_in_modules locstr dirs s =
 
 let check_required_library d =
   let d' = List.map Id.of_string d in
-  let dir = make_dirpath (List.rev d') in
+  let dir = Dir_path.make (List.rev d') in
   let mp = (fst(Lib.current_prefix())) in
   let current_dir = match mp with
-    | MPfile dp -> dir_path_eq dir dp
+    | MPfile dp -> Dir_path.equal dir dp
     | _ -> false
   in
   if not (Library.library_is_loaded dir) then
@@ -75,10 +75,10 @@ let check_required_library d =
 (* Loading silently ...
     let m, prefix = List.sep_last d' in
     read_library
-     (Loc.ghost,make_qualid (make_dirpath (List.rev prefix)) m)
+     (Loc.ghost,make_qualid (Dir_path.make (List.rev prefix)) m)
 *)
 (* or failing ...*)
-      error ("Library "^(string_of_dirpath dir)^" has to be required first.")
+      error ("Library "^(Dir_path.to_string dir)^" has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects *)
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 33392da0e..02174c876 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -54,8 +54,8 @@ val check_required_library : string list -> unit
 (** {6 Global references } *)
 
 (** Modules *)
-val logic_module : dir_path
-val logic_type_module : dir_path
+val logic_module : Dir_path.t
+val logic_type_module : Dir_path.t
 
 val datatypes_module_name : string list
 val logic_module_name : string list
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 6ea0d09a4..23c1b2abc 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -133,8 +133,8 @@ let add_glob_gen loc sp lib_dp ty =
     let mod_dp,id = Libnames.repr_path sp in
     let mod_dp = remove_sections mod_dp in
     let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
-    let filepath = Names.string_of_dirpath lib_dp in
-    let modpath = Names.string_of_dirpath mod_dp_trunc in
+    let filepath = Names.Dir_path.to_string lib_dp in
+    let modpath = Names.Dir_path.to_string mod_dp_trunc in
     let ident = Names.Id.to_string id in
       dump_ref loc filepath modpath ident ty
 
@@ -160,12 +160,12 @@ let dump_binding loc id = ()
 let dump_definition (loc, id) sec s =
   let bl,el = interval loc in
   dump_string (Printf.sprintf "%s %d:%d %s %s\n" s bl el
-			(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.Id.to_string id))
+			(Names.Dir_path.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id))
 
 let dump_reference loc modpath ident ty =
   let bl,el = interval loc in
   dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
-		  bl el (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
+		  bl el (Names.Dir_path.to_string (Lib.library_dp ())) modpath ident ty)
 
 let dump_constraint ((loc, n), _, _) sec ty =
   match n with
@@ -176,8 +176,8 @@ let dump_modref loc mp ty =
   if dump () then
     let (dp, l) = Lib.split_modpath mp in
     let l = if List.is_empty l then l else List.drop_last l in
-    let fp = Names.string_of_dirpath dp in
-    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
+    let fp = Names.Dir_path.to_string dp in
+    let mp = Names.Dir_path.to_string (Names.Dir_path.make l) in
     let bl,el = interval loc in
       dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
 		      bl el fp mp "<>" ty)
@@ -186,13 +186,13 @@ let dump_moddef loc mp ty =
   if dump () then
     let bl,el = interval loc in
     let (dp, l) = Lib.split_modpath mp in
-    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
+    let mp = Names.Dir_path.to_string (Names.Dir_path.make l) in
       dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el "<>" mp)
 
 let dump_libref loc dp ty =
   let bl,el = interval loc in
   dump_string (Printf.sprintf "R%d:%d %s <> <> %s\n"
-		  bl el (Names.string_of_dirpath dp) ty)
+		  bl el (Names.Dir_path.to_string dp) ty)
 
 let cook_notation df sc =
   (* We encode notations so that they are space-free and still human-readable *)
@@ -234,12 +234,12 @@ let cook_notation df sc =
 let dump_notation (loc,(df,_)) sc sec =
   (* We dump the location of the opening '"' *)
   dump_string (Printf.sprintf "not %d %s %s\n" (fst (Loc.unloc loc))
-    (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc))
+    (Names.Dir_path.to_string (Lib.current_dirpath sec)) (cook_notation df sc))
 
 let dump_notation_location posl df (((path,secpath),_),sc) =
   if dump () then
-    let path = Names.string_of_dirpath path in
-    let secpath = Names.string_of_dirpath secpath in
+    let path = Names.Dir_path.to_string path in
+    let secpath = Names.Dir_path.to_string secpath in
     let df = cook_notation df sc in
     List.iter (fun (bl,el) ->
       dump_string(Printf.sprintf "R%d:%d %s %s %s not\n" bl el path secpath df))
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 4a0752a3a..7674322c3 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -29,7 +29,7 @@ val dump_definition : Loc.t * Names.Id.t -> bool -> string -> unit
 val dump_moddef : Loc.t -> Names.module_path -> string -> unit
 val dump_modref  : Loc.t -> Names.module_path -> string -> unit
 val dump_reference  : Loc.t -> string -> string -> string -> unit
-val dump_libref : Loc.t -> Names.dir_path -> string -> unit
+val dump_libref : Loc.t -> Names.Dir_path.t -> string -> unit
 val dump_notation_location : (int * int) list -> Constrexpr.notation ->
   (Notation.notation_location * Notation_term.scope_name option) -> unit
 val dump_binding : Loc.t -> Names.Id.Set.elt -> unit
diff --git a/interp/notation.ml b/interp/notation.ml
index d5aa59788..39a664a64 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -44,14 +44,14 @@ open Ppextend
 
 type level = precedence * tolerability list
 type delimiters = string
-type notation_location = (dir_path * dir_path) * string
+type notation_location = (Dir_path.t * Dir_path.t) * string
 
 type scope = {
   notations: (string, interpretation * notation_location) Gmap.t;
   delimiters: delimiters option
 }
 
-(* Uninterpreted notation map: notation -> level * dir_path *)
+(* Uninterpreted notation map: notation -> level * Dir_path.t *)
 let notation_level_map = ref Gmap.empty
 
 (* Scopes table: scope_name -> symbol_interpretation *)
@@ -397,7 +397,7 @@ let find_prim_token g loc p sc =
   (* Try for a primitive numerical notation *)
   let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
   check_required_module loc sc spdir;
-  g (interp ()), ((dirpath (fst spdir),empty_dirpath),"")
+  g (interp ()), ((dirpath (fst spdir),Dir_path.empty),"")
 
 let interp_prim_token_gen g loc p local_scopes =
   let scopes = make_current_scopes local_scopes in
diff --git a/interp/notation.mli b/interp/notation.mli
index c3106f5d3..8b2d8aa0f 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -65,7 +65,7 @@ val find_delimiters_scope : Loc.t -> delimiters -> scope_name
    negative numbers are not supported, the interpreter must fail with
    an appropriate error message *)
 
-type notation_location = (dir_path * dir_path) * string
+type notation_location = (Dir_path.t * Dir_path.t) * string
 type required_module = full_path * string list
 type cases_pattern_status = bool (** true = use prim token in patterns *)
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 254805f6a..a07b6aa69 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -42,7 +42,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
 let is_alias_of_already_visible_name sp = function
   | _,NRef ref ->
       let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in
-      dir_path_eq dir empty_dirpath && Id.equal id (basename sp)
+      Dir_path.equal dir Dir_path.empty && Id.equal id (basename sp)
   | _ ->
       false
 
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 26ab4b666..08063cf2a 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -167,7 +167,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
 
   (* For syntax extensions *)
   | TacAlias of Loc.t * string *
-      (Id.t * 'lev generic_argument) list * (dir_path * glob_tactic_expr)
+      (Id.t * 'lev generic_argument) list * (Dir_path.t * glob_tactic_expr)
 
 (** Possible arguments of a tactic definition *)
 
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 16175be0d..8088ba92a 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -38,11 +38,11 @@ type printable =
   | PrintSectionContext of reference
   | PrintInspect of int
   | PrintGrammar of string
-  | PrintLoadPath of dir_path option
+  | PrintLoadPath of Dir_path.t option
   | PrintModules
   | PrintModule of reference
   | PrintModuleType of reference
-  | PrintNamespace of dir_path
+  | PrintNamespace of Dir_path.t
   | PrintMLLoadPath
   | PrintMLModules
   | PrintName of reference or_by_notation
@@ -290,7 +290,7 @@ type vernac_expr =
 
   (* Auxiliary file and library management *)
   | VernacRequireFrom of export_flag option * string
-  | VernacAddLoadPath of rec_flag * string * dir_path option
+  | VernacAddLoadPath of rec_flag * string * Dir_path.t option
   | VernacRemoveLoadPath of string
   | VernacAddMLPath of rec_flag * string
   | VernacDeclareMLModule of locality_flag * string list
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 864d2f45a..2f031c11a 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -25,9 +25,9 @@ open Environ
 
 type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
 
-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 pop_mind kn =
   let (mp,dir,l) = Names.repr_mind kn in
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 2d6317967..ffd588e57 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -373,7 +373,7 @@ if Int.equal nmr 0 then 0 else
   in find 0 (n-1) (lpar,List.rev hyps)
 
 let lambda_implicit_lift n a =
-  let level = UniverseLevel.make (make_dirpath [Id.of_string "implicit"]) 0 in
+  let level = UniverseLevel.make (Dir_path.make [Id.of_string "implicit"]) 0 in
   let implicit_sort = mkType (Universe.make level) in
   let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
   iterate lambda_implicit n (lift n a)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 51b4ca39c..b81627f22 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -259,7 +259,7 @@ let add_retroknowledge mp =
 
 let rec add_signature mp sign resolver env = 
   let add_one env (l,elem) =
-    let kn = make_kn mp empty_dirpath l in
+    let kn = make_kn mp Dir_path.empty l in
     match elem with
       | SFBconst cb ->
 	Environ.add_constant (constant_of_delta_kn resolver kn) cb env
@@ -284,7 +284,7 @@ let strengthen_const mp_from l cb resolver =
   match cb.const_body with
     | Def _ -> cb
     | _ ->
-      let kn = make_kn mp_from empty_dirpath l in
+      let kn = make_kn mp_from Dir_path.empty l in
       let con = constant_of_delta_kn resolver kn in
       { cb with
 	const_body = Def (Declarations.from_val (mkConst con));
@@ -429,8 +429,8 @@ and strengthen_and_subst_struct
 	    (* If we are performing an inclusion we need to add
 	       the fact that the constant mp_to.l is \Delta-equivalent
 	       to resolver(mp_from.l) *)
-	  let kn_from = make_kn mp_from empty_dirpath l in
-	  let kn_to = make_kn mp_to empty_dirpath l in
+	  let kn_from = make_kn mp_from Dir_path.empty l in
+	  let kn_to = make_kn mp_to Dir_path.empty l in
 	  let old_name = kn_of_delta resolver kn_from in
 	  (add_kn_delta_resolver kn_to old_name resolve_out),
 	  item'::rest'
@@ -446,8 +446,8 @@ and strengthen_and_subst_struct
 	  strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
 	if incl then
-	  let kn_from = make_kn mp_from empty_dirpath l in
-	  let kn_to = make_kn mp_to empty_dirpath l in
+	  let kn_from = make_kn mp_from Dir_path.empty l in
+	  let kn_to = make_kn mp_to Dir_path.empty l in
 	  let old_name = kn_of_delta resolver kn_from in
 	  (add_kn_delta_resolver kn_to old_name resolve_out),
 	  item'::rest'
diff --git a/kernel/names.ml b/kernel/names.ml
index dad51b51f..e10b34eb2 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -99,46 +99,87 @@ let name_eq n1 n2 = match n1, n2 with
 | Name id1, Name id2 -> String.equal id1 id2
 | _ -> false
 
+type module_ident = Id.t
+
+module ModIdmap = Idmap
+
 (** {6 Directory paths = section names paths } *)
 
 (** Dirpaths are lists of module identifiers.
     The actual representation is reversed to optimise sharing:
     Coq.A.B is ["B";"A";"Coq"] *)
 
-type module_ident = Id.t
-type dir_path = module_ident list
+let default_module_name = "If you see this, it's a bug"
 
-module ModIdmap = Idmap
+module Dir_path =
+struct
+  type t = module_ident list
+
+  let rec compare (p1 : t) (p2 : t) =
+    if p1 == p2 then 0
+    else begin match p1, p2 with
+    | [], [] -> 0
+    | [], _ -> -1
+    | _, [] -> 1
+    | id1 :: p1, id2 :: p2 ->
+      let c = Id.compare id1 id2 in
+      if Int.equal c 0 then compare p1 p2 else c
+    end
+
+  let equal p1 p2 = Int.equal (compare p1 p2) 0
+
+  let make x = x
+  let repr x = x
+
+  let empty = []
+
+  let is_empty d = match d with [] -> true | _ -> false
+
+  let to_string = function
+    | [] -> "<>"
+    | sl -> String.concat "." (List.rev_map Id.to_string sl)
+
+  let initial = [default_module_name]
+
+  module Self_Hashcons =
+    struct
+      type t_ = t
+      type t = t_
+      type u = Id.t -> Id.t
+      let hashcons hident d = List.smartmap hident d
+      let rec equal d1 d2 =
+        d1 == d2 ||
+        match (d1, d2) with
+        | [], [] -> true
+        | id1 :: d1, id2 :: d2 -> id1 == id2 && equal d1 d2
+        | _ -> false
+      let hash = Hashtbl.hash
+    end
 
-let rec dir_path_ord (p1 : dir_path) (p2 : dir_path) =
-  if p1 == p2 then 0
-  else begin match p1, p2 with
-  | [], [] -> 0
-  | [], _ -> -1
-  | _, [] -> 1
-  | id1 :: p1, id2 :: p2 ->
-    let c = Id.compare id1 id2 in
-    if Int.equal c 0 then dir_path_ord p1 p2 else c
-  end
+  module Hdir = Hashcons.Make(Self_Hashcons)
 
-let dir_path_eq p1 p2 = Int.equal (dir_path_ord p1 p2) 0
+  let hcons = Hashcons.simple_hcons Hdir.generate Id.hcons
 
-let make_dirpath x = x
-let repr_dirpath x = x
+end
 
-let empty_dirpath = []
-let is_empty_dirpath d = match d with [] -> true | _ -> false
+(** Compatibility layer for [Dir_path] *)
 
-(** Printing of directory paths as ["coq_root.module.submodule"] *)
+type dir_path = Dir_path.t
+let dir_path_ord = Dir_path.compare
+let dir_path_eq = Dir_path.equal
+let make_dirpath = Dir_path.make
+let repr_dirpath = Dir_path.repr
+let empty_dirpath = Dir_path.empty
+let is_empty_dirpath = Dir_path.is_empty
+let string_of_dirpath = Dir_path.to_string
+let initial_dir = Dir_path.initial
 
-let string_of_dirpath = function
-  | [] -> "<>"
-  | sl -> String.concat "." (List.rev_map string_of_id sl)
+(** / End of compatibility layer for [Dir_path] *)
 
 (** {6 Unique names for bound modules } *)
 
 let u_number = ref 0
-type uniq_ident = int * Id.t * dir_path
+type uniq_ident = int * Id.t * Dir_path.t
 let make_uid dir s = incr u_number;(!u_number,s,dir)
  let debug_string_of_uid (i,s,p) =
  "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
@@ -155,7 +196,7 @@ let uniq_ident_ord (x : uniq_ident) (y : uniq_ident) =
       let ans = Id.compare idl idr in
       if not (Int.equal ans 0) then ans
       else
-        dir_path_ord dpl dpr
+        Dir_path.compare dpl dpr
 
 module UOrdered =
 struct
@@ -191,7 +232,7 @@ module Labmap = Idmap
 (** {6 The module part of the kernel name } *)
 
 type module_path =
-  | MPfile of dir_path
+  | MPfile of Dir_path.t
   | MPbound of mod_bound_id
   | MPdot of module_path * label
 
@@ -210,7 +251,7 @@ let rec mp_ord mp1 mp2 =
   if mp1 == mp2 then 0
   else match (mp1, mp2) with
   | MPfile p1, MPfile p2 ->
-    dir_path_ord p1 p2
+    Dir_path.compare p1 p2
   | MPbound id1, MPbound id2 ->
     uniq_ident_ord id1 id2
   | MPdot (mp1, l1), MPdot (mp2, l2) ->
@@ -232,14 +273,11 @@ end
 module MPset = Set.Make(MPord)
 module MPmap = Map.Make(MPord)
 
-let default_module_name = "If you see this, it's a bug"
-
-let initial_dir = make_dirpath [default_module_name]
-let initial_path = MPfile initial_dir
+let initial_path = MPfile Dir_path.initial
 
 (** {6 Kernel names } *)
 
-type kernel_name = module_path * dir_path * label
+type kernel_name = module_path * Dir_path.t * label
 
 let make_kn mp dir l = (mp,dir,l)
 let repr_kn kn = kn
@@ -267,7 +305,7 @@ let kn_ord (kn1 : kernel_name) (kn2 : kernel_name) =
     let c = String.compare l1 l2 in
       if not (Int.equal c 0) then c
       else
-        let c = dir_path_ord dir1 dir2 in
+        let c = Dir_path.compare dir1 dir2 in
         if not (Int.equal c 0) then c
         else MPord.compare mp1 mp2
 
@@ -442,24 +480,10 @@ module Hname = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
-module Hdir = Hashcons.Make(
-  struct
-    type t = dir_path
-    type u = Id.t -> Id.t
-    let hashcons hident d = List.smartmap hident d
-    let rec equal d1 d2 =
-      (d1==d2) ||
-      match (d1,d2) with
-      | [],[] -> true
-      | id1::d1,id2::d2 -> id1 == id2 & equal d1 d2
-      | _ -> false
-    let hash = Hashtbl.hash
-  end)
-
 module Huniqid = Hashcons.Make(
   struct
     type t = uniq_ident
-    type u = (Id.t -> Id.t) * (dir_path -> dir_path)
+    type u = (Id.t -> Id.t) * (Dir_path.t -> Dir_path.t)
     let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
     let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
       (x == y) ||
@@ -470,7 +494,7 @@ module Huniqid = Hashcons.Make(
 module Hmod = Hashcons.Make(
   struct
     type t = module_path
-    type u = (dir_path -> dir_path) * (uniq_ident -> uniq_ident) *
+    type u = (Dir_path.t -> Dir_path.t) * (uniq_ident -> uniq_ident) *
 	(string -> string)
     let rec hashcons (hdir,huniqid,hstr as hfuns) = function
       | MPfile dir -> MPfile (hdir dir)
@@ -490,7 +514,7 @@ module Hkn = Hashcons.Make(
   struct
     type t = kernel_name
     type u = (module_path -> module_path)
-	* (dir_path -> dir_path) * (string -> string)
+	* (Dir_path.t -> Dir_path.t) * (string -> string)
     let hashcons (hmod,hdir,hstr) (md,dir,l) =
       (hmod md, hdir dir, hstr l)
     let equal (mod1,dir1,l1) (mod2,dir2,l2) =
@@ -530,11 +554,10 @@ module Hconstruct = Hashcons.Make(
   end)
 
 let hcons_name = Hashcons.simple_hcons Hname.generate Id.hcons
-let hcons_dirpath = Hashcons.simple_hcons Hdir.generate Id.hcons
-let hcons_uid = Hashcons.simple_hcons Huniqid.generate (Id.hcons,hcons_dirpath)
+let hcons_uid = Hashcons.simple_hcons Huniqid.generate (Id.hcons,Dir_path.hcons)
 let hcons_mp =
-  Hashcons.simple_hcons Hmod.generate (hcons_dirpath,hcons_uid,String.hcons)
-let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,hcons_dirpath,String.hcons)
+  Hashcons.simple_hcons Hmod.generate (Dir_path.hcons,hcons_uid,String.hcons)
+let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,Dir_path.hcons,String.hcons)
 let hcons_con = Hashcons.simple_hcons Hcn.generate hcons_kn
 let hcons_mind = Hashcons.simple_hcons Hcn.generate hcons_kn
 let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind
diff --git a/kernel/names.mli b/kernel/names.mli
index c0b38666b..2f8445ef6 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -56,31 +56,48 @@ end
 
 type name = Name of Id.t | Anonymous
 type variable = Id.t
+type module_ident = Id.t
 
 val name_eq : name -> name -> bool
 
 (** {6 Directory paths = section names paths } *)
 
-type module_ident = Id.t
-module ModIdmap : Map.S with type key = module_ident
+module Dir_path :
+sig
+  type t
+  (** Type of directory paths. Essentially a list of module identifiers. The
+      order is reversed to improve sharing. E.g. A.B.C is ["C";"B";"A"] *)
 
-type dir_path
+  val equal : t -> t -> bool
+  (** Equality over directory paths. *)
 
-val dir_path_ord : dir_path -> dir_path -> int
+  val compare : t -> t -> int
+  (** Comparison over directory paths. *)
 
-val dir_path_eq : dir_path -> dir_path -> bool
+  val make : module_ident list -> t
+  (** Create a directory path. (The list must be reversed). *)
 
-(** Inner modules idents on top of list (to improve sharing).
-   For instance: A.B.C is ["C";"B";"A"] *)
-val make_dirpath : module_ident list -> dir_path
-val repr_dirpath : dir_path -> module_ident list
+  val repr : t -> module_ident list
+  (** Represent a directory path. (The result list is reversed). *)
 
-val empty_dirpath : dir_path
+  val empty : t
+  (** The empty directory path. *)
 
-val is_empty_dirpath : dir_path -> bool
+  val is_empty : t -> bool
+  (** Test whether a directory path is empty. *)
 
-(** Printing of directory paths as ["coq_root.module.submodule"] *)
-val string_of_dirpath : dir_path -> string
+  val to_string : t -> string
+  (** Print directory paths as ["coq_root.module.submodule"] *)
+
+  val initial : t
+  (** Initial "seed" of the unique identifier generator *)
+
+  val hcons : t -> t
+  (** Hashconsing of directory paths. *)
+
+end
+
+module ModIdmap : Map.S with type key = module_ident
 
 (** {6 Names of structure elements } *)
 
@@ -108,8 +125,8 @@ val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
 (** The first argument is a file name - to prevent conflict between
    different files *)
 
-val make_mbid : dir_path -> Id.t -> mod_bound_id
-val repr_mbid : mod_bound_id -> int * Id.t * dir_path
+val make_mbid : Dir_path.t -> Id.t -> mod_bound_id
+val repr_mbid : mod_bound_id -> int * Id.t * Dir_path.t
 val id_of_mbid : mod_bound_id -> Id.t
 val debug_string_of_mbid : mod_bound_id -> string
 val string_of_mbid : mod_bound_id -> string
@@ -117,7 +134,7 @@ val string_of_mbid : mod_bound_id -> string
 (** {6 The module part of the kernel name } *)
 
 type module_path =
-  | MPfile of dir_path
+  | MPfile of Dir_path.t
   | MPbound of mod_bound_id
   | MPdot of module_path * label
 
@@ -131,9 +148,6 @@ val string_of_mp : module_path -> string
 module MPset : Set.S with type elt = module_path
 module MPmap : Map.S with type key = module_path
 
-(** Initial "seed" of the unique identifier generator *)
-val initial_dir : dir_path
-
 (** Name of the toplevel structure *)
 val initial_path : module_path (** [= MPfile initial_dir] *)
 
@@ -142,8 +156,8 @@ val initial_path : module_path (** [= MPfile initial_dir] *)
 type kernel_name
 
 (** Constructor and destructor *)
-val make_kn : module_path -> dir_path -> label -> kernel_name
-val repr_kn : kernel_name -> module_path * dir_path * label
+val make_kn : module_path -> Dir_path.t -> label -> kernel_name
+val repr_kn : kernel_name -> module_path * Dir_path.t * label
 
 val modpath : kernel_name -> module_path
 val label : kernel_name -> label
@@ -186,12 +200,12 @@ module Constrmap_env : Map.S with type key = constructor
 
 val constant_of_kn : kernel_name -> constant
 val constant_of_kn_equiv : kernel_name -> kernel_name -> constant
-val make_con : module_path -> dir_path -> label -> constant
-val make_con_equiv : module_path -> module_path -> dir_path 
+val make_con : module_path -> Dir_path.t -> label -> constant
+val make_con_equiv : module_path -> module_path -> Dir_path.t 
   -> label -> constant
 val user_con : constant -> kernel_name
 val canonical_con : constant -> kernel_name
-val repr_con : constant -> module_path * dir_path * label
+val repr_con : constant -> module_path * Dir_path.t * label
 val eq_constant : constant -> constant -> bool
 val con_with_label : constant -> label -> constant
 
@@ -206,12 +220,12 @@ val debug_string_of_con : constant -> string
 
 val mind_of_kn : kernel_name -> mutual_inductive
 val mind_of_kn_equiv : kernel_name -> kernel_name -> mutual_inductive
-val make_mind : module_path -> dir_path -> label -> mutual_inductive
-val make_mind_equiv : module_path -> module_path -> dir_path 
+val make_mind : module_path -> Dir_path.t -> label -> mutual_inductive
+val make_mind_equiv : module_path -> module_path -> Dir_path.t 
   -> label -> mutual_inductive
 val user_mind : mutual_inductive -> kernel_name
 val canonical_mind : mutual_inductive -> kernel_name
-val repr_mind : mutual_inductive -> module_path * dir_path * label
+val repr_mind : mutual_inductive -> module_path * Dir_path.t * label
 val eq_mind : mutual_inductive -> mutual_inductive -> bool
 
 val string_of_mind : mutual_inductive -> string
@@ -244,7 +258,6 @@ val eq_egr : evaluable_global_reference ->  evaluable_global_reference
 (** {6 Hash-consing } *)
 
 val hcons_name : name -> name
-val hcons_dirpath : dir_path -> dir_path
 val hcons_con : constant -> constant
 val hcons_mind : mutual_inductive -> mutual_inductive
 val hcons_ind : inductive -> inductive
@@ -315,3 +328,32 @@ module Idmap  : sig
   val singleton : key -> 'a -> 'a t
 end
 (** @deprecated Same as [Id.Map]. *)
+
+(** {5 Directory paths} *)
+
+type dir_path = Dir_path.t
+(** @deprecated Alias for [Dir_path.t]. *)
+
+val dir_path_ord : dir_path -> dir_path -> int
+(** @deprecated Same as [Dir_path.compare]. *)
+
+val dir_path_eq : dir_path -> dir_path -> bool
+(** @deprecated Same as [Dir_path.equal]. *)
+
+val make_dirpath : module_ident list -> dir_path
+(** @deprecated Same as [Dir_path.make]. *)
+
+val repr_dirpath : dir_path -> module_ident list
+(** @deprecated Same as [Dir_path.repr]. *)
+
+val empty_dirpath : dir_path
+(** @deprecated Same as [Dir_path.empty]. *)
+
+val is_empty_dirpath : dir_path -> bool
+(** @deprecated Same as [Dir_path.is_empty]. *)
+
+val string_of_dirpath : dir_path -> string
+(** @deprecated Same as [Dir_path.to_string]. *)
+
+val initial_dir : Dir_path.t
+(** @deprecated Same as [Dir_path.initial]. *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8a95c9fd2..c7bc76e57 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -76,7 +76,7 @@ type modvariant =
   | NONE
   | SIG of (* funsig params *) (mod_bound_id * module_type_body) list
   | STRUCT of (* functor params *) (mod_bound_id * module_type_body) list
-  | LIBRARY of dir_path
+  | LIBRARY of Dir_path.t
 
 type module_info =
     {modpath : module_path;
@@ -90,7 +90,7 @@ let set_engagement_opt oeng env =
       Some eng -> set_engagement eng env
     | _ -> env
 
-type library_info = dir_path * Digest.t
+type library_info = Dir_path.t * Digest.t
 
 type safe_environment =
     { old : safe_environment;
@@ -271,7 +271,7 @@ let add_constant dir l decl senv =
     | ConstantEntry ce -> translate_constant senv.env kn ce
     | GlobalRecipe r ->
       let cb = translate_recipe senv.env kn r in
-      if is_empty_dirpath dir then hcons_const_body cb else cb
+      if Dir_path.is_empty dir then hcons_const_body cb else cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
@@ -482,10 +482,10 @@ let end_module l restype senv =
    let add senv ((l,elem) as field) =
      let new_name = match elem with
        | SFBconst _ ->
-	   let kn = make_kn mp_sup empty_dirpath l in
+	   let kn = make_kn mp_sup Dir_path.empty l in
 	   C (constant_of_delta_kn resolver kn)
        | SFBmind _ ->
-	   let kn = make_kn mp_sup empty_dirpath l in
+	   let kn = make_kn mp_sup Dir_path.empty l in
 	   I (mind_of_delta_kn resolver kn)
        | SFBmodule _ -> M
        | SFBmodtype _ -> MT (MPdot(senv.modinfo.modpath, l))
@@ -630,7 +630,7 @@ let set_engagement c senv =
 (* Libraries = Compiled modules *)
 
 type compiled_library =
-    dir_path * module_body * library_info list * engagement option
+    Dir_path.t * module_body * library_info list * engagement option
 
 (* We check that only initial state Require's were performed before
    [start_library] was called *)
@@ -643,10 +643,10 @@ let start_library dir senv =
   if not (is_empty senv) then
     anomaly "Safe_typing.start_library: environment should be empty";
   let dir_path,l =
-    match (repr_dirpath dir) with
+    match (Dir_path.repr dir) with
 	[] -> anomaly "Empty dirpath in Safe_typing.start_library"
       | hd::tl ->
-	  make_dirpath tl, label_of_id hd
+	  Dir_path.make tl, label_of_id hd
   in
   let mp = MPfile dir in
   let modinfo = {modpath = mp;
@@ -682,7 +682,7 @@ let export senv dir =
   begin
     match modinfo.variant with
       | LIBRARY dp ->
-	  if not (dir_path_eq dir dp) then
+	  if not (Dir_path.equal dir dp) then
 	    anomaly "We are not exporting the right library!"
       | _ ->
 	  anomaly "We are not exporting the library"
@@ -710,9 +710,9 @@ let check_imports senv needed =
       let actual_stamp = List.assoc id imports in
       if not (String.equal stamp actual_stamp) then
 	error
-	  ("Inconsistent assumptions over module "^(string_of_dirpath id)^".")
+	  ("Inconsistent assumptions over module "^(Dir_path.to_string id)^".")
     with Not_found ->
-      error ("Reference to unknown module "^(string_of_dirpath id)^".")
+      error ("Reference to unknown module "^(Dir_path.to_string id)^".")
   in
   List.iter check needed
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 71ebe15ce..bfcc3b8a9 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -43,12 +43,12 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 val add_constant :
-  dir_path -> label -> global_declaration -> safe_environment ->
+  Dir_path.t -> label -> global_declaration -> safe_environment ->
       constant * safe_environment
 
 (** Adding an inductive type *)
 val add_mind :
-  dir_path -> label -> mutual_inductive_entry -> safe_environment ->
+  Dir_path.t -> label -> mutual_inductive_entry -> safe_environment ->
     mutual_inductive * safe_environment
 
 (** Adding a module *)
@@ -101,10 +101,10 @@ val delta_of_senv : safe_environment -> delta_resolver*delta_resolver
 (** exporting and importing modules *)
 type compiled_library
 
-val start_library : dir_path -> safe_environment
+val start_library : Dir_path.t -> safe_environment
       -> module_path * safe_environment
 
-val export : safe_environment -> dir_path
+val export : safe_environment -> Dir_path.t
       -> module_path * compiled_library
 
 val import : compiled_library -> Digest.t -> safe_environment
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d278c2d0c..dbc5b01f1 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -39,7 +39,7 @@ type namedmodule =
    constructors *)
 
 let add_mib_nameobjects mp l mib map =
-  let ind = make_mind mp empty_dirpath l in
+  let ind = make_mind mp Dir_path.empty l in
   let add_mip_nameobjects j oib map =
     let ip = (ind,j) in
     let map =
@@ -88,8 +88,8 @@ let check_conv_error error why cst f env a1 a2 =
 (* for now we do not allow reorderings *)
 
 let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= 
-  let kn1 = make_mind mp1 empty_dirpath l in
-  let kn2 = make_mind mp2 empty_dirpath l in
+  let kn1 = make_mind mp1 Dir_path.empty l in
+  let kn2 = make_mind mp2 Dir_path.empty l in
   let error why = error_signature_mismatch l spec2 why in
   let check_conv why cst f = check_conv_error error why cst f in
   let mib1 =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 1d71fd672..71b417624 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -33,10 +33,10 @@ module UniverseLevel = struct
 
   type t =
     | Set
-    | Level of int * Names.dir_path
+    | Level of int * Names.Dir_path.t
 
   (* A specialized comparison function: we compare the [int] part first.
-     This way, most of the time, the [dir_path] part is not considered.
+     This way, most of the time, the [Dir_path.t] part is not considered.
 
      Normally, placing the [int] first in the pair above in enough in Ocaml,
      but to be sure, we write below our own comparison function.
@@ -53,19 +53,19 @@ module UniverseLevel = struct
     | Level (i1, dp1), Level (i2, dp2) ->
       if i1 < i2 then -1
       else if i1 > i2 then 1
-      else Names.dir_path_ord dp1 dp2)
+      else Names.Dir_path.compare dp1 dp2)
 
   let equal u v = match u,v with
     | Set, Set -> true
     | Level (i1, dp1), Level (i2, dp2) ->
-      Int.equal i1 i2 && Int.equal (Names.dir_path_ord dp1 dp2) 0
+      Int.equal i1 i2 && Int.equal (Names.Dir_path.compare dp1 dp2) 0
     | _ -> false
 
   let make m n = Level (n, m)
 
   let to_string = function
     | Set -> "Set"
-    | Level (n,d) -> Names.string_of_dirpath d^"."^string_of_int n
+    | Level (n,d) -> Names.Dir_path.to_string d^"."^string_of_int n
 end
 
 module UniverseLMap = Map.Make (UniverseLevel)
@@ -776,7 +776,7 @@ let bellman_ford bottom g =
     graph already contains [Type.n] nodes (calling a module Type is
     probably a bad idea anyway). *)
 let sort_universes orig =
-  let mp = Names.make_dirpath [Names.Id.of_string "Type"] in
+  let mp = Names.Dir_path.make [Names.Id.of_string "Type"] in
   let rec make_level accu g i =
     let type0 = UniverseLevel.Level (i, mp) in
     let distances = bellman_ford type0 g in
@@ -837,7 +837,7 @@ let sort_universes orig =
 (* Temporary inductive type levels *)
 
 let fresh_level =
-  let n = ref 0 in fun () -> incr n; UniverseLevel.Level (!n, Names.make_dirpath [])
+  let n = ref 0 in fun () -> incr n; UniverseLevel.Level (!n, Names.Dir_path.make [])
 
 let fresh_local_univ () = Atom (fresh_level ())
 
@@ -971,7 +971,7 @@ module Hunivlevel =
   Hashcons.Make(
     struct
       type t = universe_level
-      type u = Names.dir_path -> Names.dir_path
+      type u = Names.Dir_path.t -> Names.Dir_path.t
       let hashcons hdir = function
 	| UniverseLevel.Set -> UniverseLevel.Set
 	| UniverseLevel.Level (n,d) -> UniverseLevel.Level (n,hdir d)
@@ -1004,7 +1004,7 @@ module Huniv =
       let hash = Hashtbl.hash
     end)
 
-let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.hcons_dirpath
+let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.Dir_path.hcons
 let hcons_univ = Hashcons.simple_hcons Huniv.generate hcons_univlevel
 
 module Hconstraint =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 860e3f155..b466057a2 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -20,7 +20,7 @@ sig
   val equal : t -> t -> bool
   (** Equality function *)
 
-  val make : Names.dir_path -> int -> t
+  val make : Names.Dir_path.t -> int -> t
   (** Create a new universe level from a unique identifier and an associated
       module path. *)
 
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 *)
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index bbc4a0c5a..0677fa8df 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -248,7 +248,7 @@ type tactic_grammar = {
   tacgram_key : string;
   tacgram_level : int;
   tacgram_prods : grammar_prod_item list;
-  tacgram_tactic : dir_path * Tacexpr.glob_tactic_expr;
+  tacgram_tactic : Dir_path.t * Tacexpr.glob_tactic_expr;
 }
 
 type all_grammar_command =
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 827e7c197..1cc890158 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -43,7 +43,7 @@ type tactic_grammar = {
   tacgram_key : string;
   tacgram_level : int;
   tacgram_prods : grammar_prod_item list;
-  tacgram_tactic : dir_path * Tacexpr.glob_tactic_expr;
+  tacgram_tactic : Dir_path.t * Tacexpr.glob_tactic_expr;
 }
 
 (** Adding notations *)
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 8e52a3bab..5f75a1d9e 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -18,7 +18,7 @@ let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"]
 let _ = List.iter Lexer.add_keyword prim_kw
 
 
-let local_make_qualid l id = make_qualid (make_dirpath l) id
+let local_make_qualid l id = make_qualid (Dir_path.make l) id
 
 let my_int_of_string loc s =
   try
@@ -101,7 +101,7 @@ GEXTEND Gram
   ;
   dirpath:
     [ [ id = ident; l = LIST0 field ->
-        make_dirpath (List.rev (id::l)) ] ]
+        Dir_path.make (List.rev (id::l)) ] ]
   ;
   string:
     [ [ s = STRING -> s ] ]
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index d1fd1edc7..a5f99a40b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -174,7 +174,7 @@ module Prim :
     val reference : reference Gram.entry
     val by_notation : (Loc.t * string * string option) Gram.entry
     val smart_global : reference or_by_notation Gram.entry
-    val dirpath : dir_path Gram.entry
+    val dirpath : Dir_path.t Gram.entry
     val ne_string : string Gram.entry
     val ne_lstring : string located Gram.entry
     val var : Id.t located Gram.entry
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 3269befdb..bd5e2291a 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -584,7 +584,7 @@ let pp_module mp =
     the constants are directly turned into chars *)
 
 let mk_ind path s =
-  make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
+  make_mind (MPfile (dirpath_of_string path)) Dir_path.empty (mk_label s)
 
 let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3cd3f7f8a..754016715 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -219,13 +219,13 @@ let env_for_mtb_with_def env mp seb idl =
 let rec extract_sfb_spec env mp = function
   | [] -> []
   | (l,SFBconst cb) :: msig ->
-      let kn = make_con mp empty_dirpath l in
+      let kn = make_con mp Dir_path.empty l in
       let s = extract_constant_spec env kn cb in
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmind _) :: msig ->
-      let mind = make_mind mp empty_dirpath l in
+      let mind = make_mind mp Dir_path.empty l in
       let s = Sind (mind, extract_inductive env mind) in
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs
@@ -288,7 +288,7 @@ let rec extract_sfb env mp all = function
   | (l,SFBconst cb) :: msb ->
       (try
 	 let vl,recd,msb = factor_fix env l cb msb in
-	 let vc = Array.map (make_con mp empty_dirpath) vl in
+	 let vc = Array.map (make_con mp Dir_path.empty) vl in
 	 let ms = extract_sfb env mp all msb in
 	 let b = Array.exists Visit.needed_con vc in
 	 if all || b then
@@ -298,7 +298,7 @@ let rec extract_sfb env mp all = function
 	 else ms
        with Impossible ->
 	 let ms = extract_sfb env mp all msb in
-	 let c = make_con mp empty_dirpath l in
+	 let c = make_con mp Dir_path.empty l in
 	 let b = Visit.needed_con c in
 	 if all || b then
 	   let d = extract_constant env c cb in
@@ -307,7 +307,7 @@ let rec extract_sfb env mp all = function
 	 else ms)
   | (l,SFBmind mib) :: msb ->
       let ms = extract_sfb env mp all msb in
-      let mind = make_mind mp empty_dirpath l in
+      let mind = make_mind mp Dir_path.empty l in
       let b = Visit.needed_ind mind in
       if all || b then
 	let d = Dind (mind, extract_inductive env mind) in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index d8d1d1eae..bcdee5954 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1304,9 +1304,9 @@ let inline_test r t =
        not (is_fix t2) && ml_size t < 12 && is_not_strict t)
 
 let con_of_string s =
-  let null = empty_dirpath in
-  match repr_dirpath (dirpath_of_string s) with
-    | id :: d -> make_con (MPfile (make_dirpath d)) null (label_of_id id)
+  let null = Dir_path.empty in
+  match Dir_path.repr (dirpath_of_string s) with
+    | id :: d -> make_con (MPfile (Dir_path.make d)) null (label_of_id id)
     | [] -> assert false
 
 let manual_inline_set =
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index ca72a38ed..9746c39e4 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -34,7 +34,7 @@ let se_iter do_decl do_spec do_mp =
 	let mp_w =
 	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
 	in
-	let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
+	let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l')) in
 	mt_iter mt; do_decl (Dtype(r,l,t))
     | MTwith (mt,ML_With_module(idl,mp))->
         let mp_mt = msid_of_mt mt in
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index b8d75d445..7742dd783 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -650,7 +650,7 @@ and pp_module_type params = function
       let mp_w =
 	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
       in
-      let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l)) in
+      let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l)) in
       push_visible mp_mt [];
       let pp_w = str " with type " ++ ids ++ pp_global Type r in
       pop_visible();
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index c7d8d42de..a54121139 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -56,7 +56,7 @@ let is_modfile = function
   | _ -> false
 
 let raw_string_of_modfile = function
-  | MPfile f -> String.capitalize (Id.to_string (List.hd (repr_dirpath f)))
+  | MPfile f -> String.capitalize (Id.to_string (List.hd (Dir_path.repr f)))
   | _ -> assert false
 
 let current_toplevel () = fst (Lib.current_prefix ())
@@ -175,7 +175,7 @@ let add_recursors env kn =
     make_con_equiv
       (modpath (user_mind kn))
       (modpath (canonical_mind kn))
-      empty_dirpath (label_of_id id)
+      Dir_path.empty (label_of_id id)
   in
   let mib = Environ.lookup_mind kn env in
   Array.iter
@@ -272,7 +272,7 @@ let safe_pr_long_global r =
     | _ -> assert false
 
 let pr_long_mp mp =
-  let lid = repr_dirpath (Nametab.dirpath_of_module mp) in
+  let lid = Dir_path.repr (Nametab.dirpath_of_module mp) in
   str (String.concat "." (List.map Id.to_string (List.rev lid)))
 
 let pr_long_global ref = pr_path (Nametab.path_of_global ref)
@@ -424,7 +424,7 @@ let check_loaded_modfile mp = match base_mp mp with
       if not (Library.library_is_loaded dp) then begin
 	match base_mp (current_toplevel ()) with
 	  | MPfile dp' when dp<>dp' ->
-	      err (str ("Please load library "^(string_of_dirpath dp^" first.")))
+	      err (str ("Please load library "^(Dir_path.to_string dp^" first.")))
 	  | _ -> ()
       end
   | _ -> ()
@@ -727,7 +727,7 @@ let string_of_modfile mp =
 
 let file_of_modfile mp =
   let s0 = match mp with
-    | MPfile f -> Id.to_string (List.hd (repr_dirpath f))
+    | MPfile f -> Id.to_string (List.hd (Dir_path.repr f))
     | _ -> assert false
   in
   let s = String.copy (string_of_modfile mp) in
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index fbf48889f..2cf3c475e 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -46,7 +46,7 @@ val info_file : string -> unit
 (*s utilities about [module_path] and [kernel_names] and [global_reference] *)
 
 val occur_kn_in_ref : mutual_inductive -> global_reference -> bool
-val repr_of_r : global_reference -> module_path * dir_path * label
+val repr_of_r : global_reference -> module_path * Dir_path.t * label
 val modpath_of_r : global_reference -> module_path
 val label_of_r : global_reference -> label
 val current_toplevel : unit -> module_path
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index f8b1927a3..455f3539b 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -81,8 +81,8 @@ type ineq = Rlt | Rle | Rgt | Rge
 let string_of_R_constant kn =
   match Names.repr_con kn with
     | MPfile dir, sec_dir, id when
-	sec_dir = empty_dirpath &&
-	string_of_dirpath dir = "Coq.Reals.Rdefinitions"
+	sec_dir = Dir_path.empty &&
+	Dir_path.to_string dir = "Coq.Reals.Rdefinitions"
 	-> string_of_label id
     | _ -> "constant_not_of_R"
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f922b2f60..3dfce8bf4 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -460,7 +460,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
     match wf_rel_expr_opt with 
       | None ->
 	  let ltof =
-	    let make_dir l = make_dirpath (List.map Id.of_string (List.rev l)) in
+	    let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l)) in
 	    Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path
 			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
 	  in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 2d50adf00..5942e11b4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -132,7 +132,7 @@ let coq_constant s =
     Coqlib.init_modules s;;
 
 let find_reference sl s =
-    (Nametab.locate (make_qualid(Names.make_dirpath
+    (Nametab.locate (make_qualid(Names.Dir_path.make
 			   (List.map Id.of_string (List.rev sl)))
 	       (Id.of_string s)));;
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 28752fe4f..68c5e16ae 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -50,7 +50,7 @@ let coq_base_constant s =
     (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
 
 let find_reference sl s =
-    (locate (make_qualid(Names.make_dirpath
+    (locate (make_qualid(Names.Dir_path.make
 			   (List.map Id.of_string (List.rev sl)))
 	       (Id.of_string s)));;
 
@@ -85,7 +85,7 @@ let type_of_const t =
 
 let constant sl s =
   constr_of_global
-    (locate (make_qualid(Names.make_dirpath
+    (locate (make_qualid(Names.Dir_path.make
 			   (List.map Id.of_string (List.rev sl)))
 	       (Id.of_string s)));;
 let const_of_ref = function
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 92135d497..11281f114 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -19,7 +19,7 @@ let meaningful_submodule = [ "Z"; "N"; "Pos" ]
 
 let string_of_global r =
   let dp = Nametab.dirpath_of_global r in
-  let prefix = match Names.repr_dirpath dp with
+  let prefix = match Names.Dir_path.repr dp with
     | [] -> ""
     | m::_ ->
       let s = Names.Id.to_string m in
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 17ea6f2bf..d02d26007 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -244,13 +244,13 @@ let my_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)
 
 let new_ring_path =
-  make_dirpath (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
+  Dir_path.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let ltac s =
-  lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile new_ring_path) (Dir_path.make []) (mk_label s))
 let znew_ring_path =
-  make_dirpath (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
+  Dir_path.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
-  lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile znew_ring_path) (Dir_path.make []) (mk_label s))
 
 let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
@@ -826,10 +826,10 @@ END
 (***********************************************************************)
 
 let new_field_path =
-  make_dirpath (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
+  Dir_path.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
-  lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s))
+  lazy(make_kn (MPfile new_field_path) (Dir_path.make []) (mk_label s))
 
 
 let _ = add_map "field"
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 958fdc649..601a4ffd1 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -16,7 +16,7 @@ open Coqlib
 
 exception Non_closed_ascii
 
-let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
 let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index f86b56bc7..d6b9f73d5 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -14,10 +14,10 @@ open Glob_term
 
 (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
 
-let make_dir l = Names.make_dirpath (List.map Names.Id.of_string (List.rev l))
+let make_dir l = Names.Dir_path.make (List.map Names.Id.of_string (List.rev l))
 let make_path dir id = Libnames.make_path (make_dir dir) (Names.Id.of_string id)
 
-let make_mind mp id = Names.make_mind mp Names.empty_dirpath (Names.mk_label id)
+let make_mind mp id = Names.make_mind mp Names.Dir_path.empty (Names.mk_label id)
 let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id
 let make_mind_mpdot dir modname id =
   let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.mk_label modname)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index f7d0091f3..d84fad6ff 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -19,7 +19,7 @@ exception Non_closed_number
 open Glob_term
 open Bigint
 
-let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
 let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
 let make_path dir id = Libnames.make_path dir (Id.of_string id)
 
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 9faa6edd1..d583f44cb 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -23,7 +23,7 @@ open Glob_term
 
 let binnums = ["Coq";"Numbers";"BinNums"]
 
-let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let positive_path = make_path binnums "positive"
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index d817396f1..fb951b35f 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -36,7 +36,7 @@ let get_module_path_of_full_path path =
 let remove_module_dirpath_from_dirpath ~basedir dir =
  let module Ln = Libnames in
   if Ln.is_dirpath_prefix_of basedir dir then
-   let ids = Names.repr_dirpath dir in
+   let ids = Names.Dir_path.repr dir in
    let rec remove_firsts n l =
     match n,l with
        (0,l) -> l
@@ -46,11 +46,11 @@ let remove_module_dirpath_from_dirpath ~basedir dir =
     let ids' =
      List.rev
       (remove_firsts
-        (List.length (Names.repr_dirpath basedir))
+        (List.length (Names.Dir_path.repr basedir))
         (List.rev ids))
     in
      ids'
-  else Names.repr_dirpath dir
+  else Names.Dir_path.repr dir
 ;;
 
 
@@ -61,7 +61,7 @@ let get_uri_of_var v pvars =
    function
       [] -> Errors.error ("Variable "^v^" not found")
     | he::tl as modules ->
-       let dirpath = N.make_dirpath modules in
+       let dirpath = N.Dir_path.make modules in
         if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then
          modules
         else
@@ -71,7 +71,7 @@ let get_uri_of_var v pvars =
     if List.mem v pvars then
       []
     else
-      search_in_open_sections (N.repr_dirpath (Lib.cwd ()))
+      search_in_open_sections (N.Dir_path.repr (Lib.cwd ()))
    in
     "cic:" ^
      List.fold_left
@@ -106,21 +106,21 @@ let ext_of_tag =
 exception FunctorsXMLExportationNotImplementedYet;;
 
 let subtract l1 l2 =
- let l1' = List.rev (Names.repr_dirpath l1) in
- let l2' = List.rev (Names.repr_dirpath l2) in
+ let l1' = List.rev (Names.Dir_path.repr l1) in
+ let l2' = List.rev (Names.Dir_path.repr l2) in
   let rec aux =
    function
       he::tl when tl = l2' -> [he]
     | he::tl -> he::(aux tl)
     | [] -> assert (l2' = []) ; []
   in
-   Names.make_dirpath (List.rev (aux l1'))
+   Names.Dir_path.make (List.rev (aux l1'))
 ;;
 
 let token_list_of_path dir id tag =
  let module N = Names in
   let token_list_of_dirpath dirpath =
-   List.rev_map N.Id.to_string (N.repr_dirpath dirpath) in
+   List.rev_map N.Id.to_string (N.Dir_path.repr dirpath) in
   token_list_of_dirpath dir @ [N.Id.to_string id ^ "." ^ (ext_of_tag tag)]
 
 let token_list_of_kernel_name tag =
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 8f1d97d3b..b4ec85ab7 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -20,7 +20,7 @@ let cprop =
   N.make_con
    (N.MPfile
      (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
-   (N.make_dirpath [])
+   (N.Dir_path.make [])
    (N.mk_label "CProp")
 ;;
 
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 35760a51d..50309317e 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -46,7 +46,7 @@ let filter_params pvars hyps =
   let cwd = Lib.cwd () in
   let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
-   aux (Names.repr_dirpath modulepath) (List.rev pvars)
+   aux (Names.Dir_path.repr modulepath) (List.rev pvars)
 ;;
 
 (* The computation is very inefficient, but we can't do anything *)
@@ -62,7 +62,7 @@ let search_variables () =
        [] -> []
      | he::tl as modules ->
         let one_section_variables =
-         let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in
+         let dirpath = N.Dir_path.make (modules @ N.Dir_path.repr modulepath) in
           let t = List.map N.Id.to_string (Decls.last_section_hyps dirpath) in
            [he,t]
         in
@@ -113,7 +113,7 @@ let theory_filename xml_library_root =
   match xml_library_root with
     None -> None  (* stdout *)
   | Some xml_library_root' ->
-     let toks = List.map N.Id.to_string (N.repr_dirpath (Lib.library_dp ())) in
+     let toks = List.map N.Id.to_string (N.Dir_path.repr (Lib.library_dp ())) in
      (* theory from A/B/C/F.v goes into A/B/C/F.theory *)
      let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")
@@ -531,7 +531,7 @@ let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;
 
 let uri_of_dirpath dir =
   "/" ^ String.concat "/"
-    (List.map Names.Id.to_string (List.rev (Names.repr_dirpath dir)))
+    (List.map Names.Id.to_string (List.rev (Names.Dir_path.repr dir)))
 ;;
 
 let _ =
@@ -550,5 +550,5 @@ let _ =
   Library.set_xml_require
     (fun d -> theory_output_string
       (Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>"
-       (uri_of_dirpath d) (Names.string_of_dirpath d)))
+       (uri_of_dirpath d) (Names.Dir_path.to_string d)))
 ;;
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index 5e725979b..a7b49fbe2 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -30,7 +30,7 @@ let is_imported_modpath mp =
     match mp with
       | MPfile dp ->
 	  let rec find_prefix = function
-	    |MPfile dp1 -> not (dir_path_eq dp1 dp)
+	    |MPfile dp1 -> not (Dir_path.equal dp1 dp)
 	    |MPdot(mp,_) -> find_prefix mp
 	    |MPbound(_) -> false
 	  in find_prefix current_mp
diff --git a/pretyping/program.ml b/pretyping/program.ml
index a0befa130..d2e22f71e 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -11,7 +11,7 @@ open Util
 open Names
 open Term
 
-let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
 
 let find_reference locstr dir s =
   let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 2cc538004..f48734be7 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -141,7 +141,7 @@ let print_env env =
   in
     (sign_env ++ db_env)
 
-(*let current_module = ref empty_dirpath
+(*let current_module = ref Dir_path.empty
 
 let set_module m = current_module := m*)
 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index dee144b95..3a5cb784e 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -331,7 +331,7 @@ let print_located_qualid ref =
   match List.map expand (N.locate_extended_all qid) with
     | [] ->
 	let (dir,id) = repr_qualid qid in
-	if dir = empty_dirpath then
+	if dir = Dir_path.empty then
 	  str "No object of basename " ++ pr_id id
 	else
 	  str "No object of suffix " ++ pr_qualid qid
@@ -634,7 +634,7 @@ let print_any_name = function
   | Undefined qid ->
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in
-    if (repr_dirpath dir) <> [] then raise Not_found;
+    if (Dir_path.repr dir) <> [] then raise Not_found;
     let (_,c,typ) = Global.lookup_named str in
     (print_named_decl (str,c,typ))
   with Not_found ->
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 44c246661..7ee5b92de 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -37,7 +37,7 @@ let _ =
 
 let get_new_id locals id =
   let rec get_id l id =
-    let dir = make_dirpath [id] in
+    let dir = Dir_path.make [id] in
       if not (Nametab.exists_module dir) then
 	id
       else
@@ -71,9 +71,9 @@ let print_kn locals kn =
 
 let nametab_register_dir mp =
   let id = Id.of_string "FAKETOP" in
-  let fp = Libnames.make_path empty_dirpath id in
-  let dir = make_dirpath [id] in
-  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)));
+  let fp = Libnames.make_path Dir_path.empty id in
+  let dir = Dir_path.make [id] in
+  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,Dir_path.empty)));
   fp
 
 (** Nota: the [global_reference] we register in the nametab below
@@ -90,9 +90,9 @@ let nametab_register_body mp fp (l,body) =
     | SFBmodule _ -> () (* TODO *)
     | SFBmodtype _ -> () (* TODO *)
     | SFBconst _ ->
-      push (id_of_label l) (ConstRef (make_con mp empty_dirpath l))
+      push (id_of_label l) (ConstRef (make_con mp Dir_path.empty l))
     | SFBmind mib ->
-      let mind = make_mind mp empty_dirpath l in
+      let mind = make_mind mp Dir_path.empty l in
       Array.iteri
 	(fun i mip ->
 	  push mip.mind_typename (IndRef (mind,i));
@@ -126,7 +126,7 @@ let print_body is_impl env mp (l,body) =
     | SFBmind mib ->
       try
 	let env = Option.get env in
-	Printer.pr_mutual_inductive_body env (make_mind mp empty_dirpath l) mib
+	Printer.pr_mutual_inductive_body env (make_mind mp Dir_path.empty l) mib
       with _ ->
 	(if mib.mind_finite then str "Inductive " else str "CoInductive")
 	++ name)
@@ -208,7 +208,7 @@ let rec print_modexpr env mp locals mexpr = match mexpr with
 
 let rec printable_body dir =
   let dir = pop_dirpath dir in
-    dir = empty_dirpath ||
+    dir = Dir_path.empty ||
     try
       match Nametab.locate_dir (qualid_of_dirpath dir) with
 	  DirOpenModtype _ -> false
diff --git a/printing/printmod.mli b/printing/printmod.mli
index b83d97f6a..afd4d37f3 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -9,7 +9,7 @@
 open Names
 
 (** false iff the module is an element of an open module type *)
-val printable_body : dir_path -> bool
+val printable_body : Dir_path.t -> bool
 
 val print_module : bool -> module_path -> Pp.std_ppcmds
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index e5fddfde2..9c27b2951 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -38,7 +38,7 @@ open Decl_kinds
 (** Typeclass-based generalized rewriting. *)
 
 let classes_dirpath =
-  make_dirpath (List.map Id.of_string ["Classes";"Coq"])
+  Dir_path.make (List.map Id.of_string ["Classes";"Coq"])
 
 let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
@@ -52,7 +52,7 @@ let proper_proxy_class =
 
 let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
 
-let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
 
 let try_find_global_reference dir s =
   let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index fbae96651..8712b291e 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -298,7 +298,7 @@ let tauto_intuitionistic flags g =
 
 let coq_nnpp_path =
   let dir = List.map Id.of_string ["Classical_Prop";"Logic";"Coq"] in
-  Libnames.make_path (make_dirpath dir) (Id.of_string "NNPP")
+  Libnames.make_path (Dir_path.make dir) (Id.of_string "NNPP")
 
 let tauto_classical flags nnpp g =
   try tclTHEN (apply nnpp) (tauto_intuitionistic flags) g
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index e40e46e69..59d73e7bd 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -56,8 +56,8 @@ let load_rcfile() =
 
 (* Puts dir in the path of ML and in the LoadPath *)
 let coq_add_path unix_path s =
-  Mltop.add_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root;Names.Id.of_string s])
-let coq_add_rec_path unix_path = Mltop.add_rec_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root])
+  Mltop.add_path ~unix_path ~coq_root:(Names.Dir_path.make [Nameops.coq_root;Names.Id.of_string s])
+let coq_add_rec_path unix_path = Mltop.add_rec_path ~unix_path ~coq_root:(Names.Dir_path.make [Nameops.coq_root])
 
 (* By the option -include -I or -R of the command line *)
 let includes = ref []
@@ -104,7 +104,7 @@ let init_load_path () =
     if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
     (* then standard library *)
     List.iter
-      (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.make_dirpath [Names.Id.of_string alias; Nameops.coq_root]))
+      (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.Dir_path.make [Names.Id.of_string alias; Nameops.coq_root]))
       theories_dirs_map;
     (* then plugins *)
     List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 9ca1deb41..0039620f0 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -15,8 +15,8 @@ val set_rcfile : string -> unit
 val no_load_rc : unit -> unit
 val load_rcfile : unit -> unit
 
-val push_include : string * Names.dir_path -> unit
-val push_rec_include : string * Names.dir_path -> unit
+val push_include : string * Names.Dir_path.t -> unit
+val push_rec_include : string * Names.Dir_path.t -> unit
 
 val init_load_path : unit -> unit
 val init_library_roots : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 90652d348..064a42cc8 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -52,10 +52,10 @@ let engage () =
 
 let set_batch_mode () = batch_mode := true
 
-let toplevel_default_name = make_dirpath [Id.of_string "Top"]
+let toplevel_default_name = Dir_path.make [Id.of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
 let set_toplevel_name dir =
-  if dir_path_eq dir empty_dirpath then error "Need a non empty toplevel module name";
+  if Dir_path.equal dir Dir_path.empty then error "Need a non empty toplevel module name";
   toplevel_name := Some dir
 let unset_toplevel_name () = toplevel_name := None
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 4f5bb148d..ae0dc708e 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -225,11 +225,11 @@ let inloadpath dir =
   Library.is_in_load_paths (CUnix.physical_path_of_string dir)
 
 let status () =
-  (** We remove the initial part of the current [dir_path]
+  (** We remove the initial part of the current [Dir_path.t]
       (usually Top in an interactive session, cf "coqtop -top"),
       and display the other parts (opened sections and modules) *)
   let path =
-    let l = Names.repr_dirpath (Lib.cwd ()) in
+    let l = Names.Dir_path.repr (Lib.cwd ()) in
     List.rev_map Names.Id.to_string l
   in
   let proof =
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 75a0a8964..0aa15edda 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -163,11 +163,11 @@ let convert_string d =
 let add_rec_path ~unix_path ~coq_root =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
-    let prefix = Names.repr_dirpath coq_root in
+    let prefix = Names.Dir_path.repr coq_root in
     let convert_dirs (lp, cp) =
       try
         let path = List.map convert_string (List.rev cp) @ prefix in
-        Some (lp, Names.make_dirpath path)
+        Some (lp, Names.Dir_path.make path)
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index e368bf997..761a52d4a 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -43,8 +43,8 @@ val add_ml_dir : string -> unit
 val add_rec_ml_dir : string -> unit
 
 (** Adds a path to the Coq and ML paths *)
-val add_path : unix_path:string -> coq_root:Names.dir_path -> unit
-val add_rec_path : unix_path:string -> coq_root:Names.dir_path -> unit
+val add_path : unix_path:string -> coq_root:Names.Dir_path.t -> unit
+val add_rec_path : unix_path:string -> coq_root:Names.Dir_path.t -> unit
 
 (** List of modules linked to the toplevel *)
 val add_known_module : string -> unit
diff --git a/toplevel/search.ml b/toplevel/search.ml
index b91b96d59..afc961596 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -118,7 +118,7 @@ let plain_display accu ref a c =
 
 let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l)
 
-let filter_by_module (module_list:dir_path list) (accept:bool)
+let filter_by_module (module_list:Dir_path.t list) (accept:bool)
   (ref:global_reference) _ _ =
     let sp = path_of_global ref in
     let sl = dirpath sp in
@@ -181,7 +181,7 @@ let name_of_reference ref = Id.to_string (basename_of_global ref)
 
 let full_name_of_reference ref =
   let (dir,id) = repr_path (path_of_global ref) in
-  string_of_dirpath dir ^ "." ^ Id.to_string id
+  Dir_path.to_string dir ^ "." ^ Id.to_string id
 
 (*
  * functions to use the new Libtypes facility
@@ -318,10 +318,10 @@ let interface_search flags =
   in
   let ans = ref [] in
   let print_function ref env constr =
-    let fullpath = repr_dirpath (Nametab.dirpath_of_global ref) in
+    let fullpath = Dir_path.repr (Nametab.dirpath_of_global ref) in
     let qualid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
     let (shortpath, basename) = Libnames.repr_qualid qualid in
-    let shortpath = repr_dirpath shortpath in
+    let shortpath = Dir_path.repr shortpath in
     (* [shortpath] is a suffix of [fullpath] and we're looking for the missing
        prefix *)
     let rec prefix full short accu = match full, short with
diff --git a/toplevel/search.mli b/toplevel/search.mli
index 56b6a1bda..919fafc6c 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -23,11 +23,11 @@ type glob_search_about_item =
 type filter_function = global_reference -> env -> constr -> bool
 type display_function = global_reference -> env -> constr -> unit
 
-val search_by_head : constr -> dir_path list * bool -> std_ppcmds
-val search_rewrite : constr -> dir_path list * bool -> std_ppcmds
-val search_pattern : constr -> dir_path list * bool -> std_ppcmds
+val search_by_head : constr -> Dir_path.t list * bool -> std_ppcmds
+val search_rewrite : constr -> Dir_path.t list * bool -> std_ppcmds
+val search_pattern : constr -> Dir_path.t list * bool -> std_ppcmds
 val search_about  :
-  (bool * glob_search_about_item) list -> dir_path list * bool -> std_ppcmds
+  (bool * glob_search_about_item) list -> Dir_path.t list * bool -> std_ppcmds
 
 val interface_search : (Interface.search_constraint * bool) list ->
   string Interface.coq_object list
@@ -35,7 +35,7 @@ val interface_search : (Interface.search_constraint * bool) list ->
 (** The filtering function that is by standard search facilities.
    It can be passed as argument to the raw search functions. *)
 
-val filter_by_module_from_list : dir_path list * bool -> filter_function
+val filter_by_module_from_list : Dir_path.t list * bool -> filter_function
 
 val filter_blacklist : filter_function
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 34aa23585..7a17a2b31 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -427,7 +427,7 @@ let load_vernac verb file =
 let compile verbosely f =
   let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
   Dumpglob.start_dump_glob long_f_dot_v;
-  Dumpglob.dump_string ("F" ^ Names.string_of_dirpath ldir ^ "\n");
+  Dumpglob.dump_string ("F" ^ Names.Dir_path.to_string ldir ^ "\n");
   if !Flags.xml_export then !xml_start_library ();
   let _ = load_vernac verbosely long_f_dot_v in
   let pfs = Pfedit.get_all_proof_names () in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 25d0fcec9..f37d99dd1 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -201,7 +201,7 @@ let show_match id =
 (* "Print" commands *)
 
 let print_path_entry (s,l) =
-  (str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s)
+  (str (Dir_path.to_string l) ++ str " " ++ tbrk (0,0) ++ str s)
 
 let print_loadpath dir =
   let l = Library.get_full_load_paths () in
@@ -250,7 +250,7 @@ let print_modtype r =
       msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid)
 
 let print_namespace ns =
-  let ns = List.rev (Names.repr_dirpath ns) in
+  let ns = List.rev (Names.Dir_path.repr ns) in
   (* [match_dirpath], [match_modulpath] are helpers for [matches]
      which checks whether a constant is in the namespace [ns]. *)
   let rec match_dirpath ns = function
@@ -266,7 +266,7 @@ let print_namespace ns =
   in
   let rec match_modulepath ns = function
     | MPbound _ -> None (* Not a proper namespace. *)
-    | MPfile dir -> match_dirpath ns (Names.repr_dirpath dir)
+    | MPfile dir -> match_dirpath ns (Names.Dir_path.repr dir)
     | MPdot (mp,lbl) ->
         let id = Names.id_of_label lbl in
         begin match match_modulepath ns mp with
@@ -286,7 +286,7 @@ let print_namespace ns =
   let qualified_minus n mp =
     let rec list_of_modulepath = function
       | MPbound _ -> assert false (* MPbound never matches *)
-      | MPfile dir -> Names.repr_dirpath dir
+      | MPfile dir -> Names.Dir_path.repr dir
       | MPdot (mp,lbl) -> (Names.id_of_label lbl)::(list_of_modulepath mp)
     in
     snd (Util.List.chop n (List.rev (list_of_modulepath mp)))
@@ -400,7 +400,7 @@ let print_located_module r =
     let dir = Nametab.full_name_module qid in
     msg_notice (str "Module " ++ pr_dirpath dir)
   with Not_found ->
-    if dir_path_eq (fst (repr_qualid qid)) empty_dirpath then
+    if Dir_path.equal (fst (repr_qualid qid)) Dir_path.empty then
       msg_error (str "No module is referred to by basename" ++ spc () ++ pr_qualid qid)
     else
       msg_error (str "No module is referred to by name" ++ spc () ++ pr_qualid qid)
@@ -729,7 +729,7 @@ let vernac_begin_section (_, id as lid) =
 
 let vernac_end_section (loc,_) =
   Dumpglob.dump_reference loc
-    (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
+    (Dir_path.to_string (Lib.current_dirpath true)) "<>" "sec";
   Lib.close_section ()
 
 (* Dispatcher of the "End" command *)
@@ -1492,7 +1492,7 @@ let vernac_reset_name id =
     if not globalized then begin
        try begin match Lib.find_opening_node (snd id) with
           | Lib.OpenedSection _ -> Dumpglob.dump_reference (fst id)
-              (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
+              (Dir_path.to_string (Lib.current_dirpath true)) "<>" "sec";
           (* Might be nice to implement module cases, too.... *)
           | _ -> ()
        end with UserError _ -> ()
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index aa3cc9485..4999cd0c2 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -83,7 +83,7 @@ let error_whelp_unknown_reference ref =
 let uri_of_repr_kn ref (mp,dir,l) =
   match mp with
     | MPfile sl ->
-        uri_of_dirpath (id_of_label l :: repr_dirpath dir @ repr_dirpath sl)
+        uri_of_dirpath (id_of_label l :: Dir_path.repr dir @ Dir_path.repr sl)
     | _ ->
         error_whelp_unknown_reference ref