Modulification of dir_path

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

10 files changed, 183 insertions, 118 deletions

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. *)