Dir_path --> DirPath

 Ok, this is merely a matter of taste, but up to now the usage
 in Coq is rather to use capital letters instead of _ in the
 names of inner modules.

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

10 files changed, 95 insertions, 95 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 4fde7474b..fb3303687 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 Dir_path.repr p with
+let pop_dirpath p = match DirPath.repr p with
   | [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath")
-  | _::l -> Dir_path.make l
+  | _::l -> DirPath.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 357a48080..d80c69bee 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 (Dir_path.make [Id.of_string "implicit"]) 0 in
+  let level = UniverseLevel.make (DirPath.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 e247a5712..48ce47bd4 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 Dir_path.empty l in
+    let kn = make_kn mp DirPath.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 Dir_path.empty l in
+      let kn = make_kn mp_from DirPath.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 Dir_path.empty l in
-	  let kn_to = make_kn mp_to Dir_path.empty l in
+	  let kn_from = make_kn mp_from DirPath.empty l in
+	  let kn_to = make_kn mp_to DirPath.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 Dir_path.empty l in
-	  let kn_to = make_kn mp_to Dir_path.empty l in
+	  let kn_from = make_kn mp_from DirPath.empty l in
+	  let kn_to = make_kn mp_to DirPath.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 e207c998e..f74240a23 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -126,7 +126,7 @@ module ModIdmap = Id.Map
 
 let default_module_name = "If you see this, it's a bug"
 
-module Dir_path =
+module DirPath =
 struct
   type t = module_ident list
 
@@ -181,7 +181,7 @@ end
 
 module MBId =
 struct
-  type t = int * Id.t * Dir_path.t
+  type t = int * Id.t * DirPath.t
 
   let gen =
     let seed = ref 0 in fun () ->
@@ -194,7 +194,7 @@ struct
   let repr mbid = mbid
 
   let to_string (i, s, p) =
-    Dir_path.to_string p ^ "." ^ s
+    DirPath.to_string p ^ "." ^ s
 
   let debug_to_string (i, s, p) =
     "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
@@ -209,7 +209,7 @@ struct
         let ans = Id.compare idl idr in
         if not (Int.equal ans 0) then ans
         else
-          Dir_path.compare dpl dpr
+          DirPath.compare dpl dpr
 
   let equal x y = Int.equal (compare x y) 0
 
@@ -219,7 +219,7 @@ struct
     struct
       type _t = t
       type t = _t
-      type u = (Id.t -> Id.t) * (Dir_path.t -> Dir_path.t)
+      type u = (Id.t -> Id.t) * (DirPath.t -> DirPath.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) ||
@@ -229,7 +229,7 @@ struct
 
   module HashMBId = Hashcons.Make(Self_Hashcons)
 
-  let hcons = Hashcons.simple_hcons HashMBId.generate (Id.hcons, Dir_path.hcons)
+  let hcons = Hashcons.simple_hcons HashMBId.generate (Id.hcons, DirPath.hcons)
 
 end
 
@@ -248,7 +248,7 @@ end
 module ModPath = struct
 
   type t =
-    | MPfile of Dir_path.t
+    | MPfile of DirPath.t
     | MPbound of MBId.t
     | MPdot of t * Label.t
 
@@ -260,7 +260,7 @@ module ModPath = struct
     | _ -> false
 
   let rec to_string = function
-    | MPfile sl -> Dir_path.to_string sl
+    | MPfile sl -> DirPath.to_string sl
     | MPbound uid -> MBId.to_string uid
     | MPdot (mp,l) -> to_string mp ^ "." ^ Label.to_string l
 
@@ -268,7 +268,7 @@ module ModPath = struct
   let rec compare mp1 mp2 =
     if mp1 == mp2 then 0
     else match mp1, mp2 with
-      | MPfile p1, MPfile p2 -> Dir_path.compare p1 p2
+      | MPfile p1, MPfile p2 -> DirPath.compare p1 p2
       | MPbound id1, MPbound id2 -> MBId.compare id1 id2
       | MPdot (mp1, l1), MPdot (mp2, l2) ->
         let c = String.compare l1 l2 in
@@ -281,11 +281,11 @@ module ModPath = struct
 
   let equal mp1 mp2 = Int.equal (compare mp1 mp2) 0
 
-  let initial = MPfile Dir_path.initial
+  let initial = MPfile DirPath.initial
 
   module Self_Hashcons = struct
     type t = module_path
-    type u = (Dir_path.t -> Dir_path.t) * (MBId.t -> MBId.t) *
+    type u = (DirPath.t -> DirPath.t) * (MBId.t -> MBId.t) *
 	(string -> string)
     let rec hashcons (hdir,huniqid,hstr as hfuns) = function
       | MPfile dir -> MPfile (hdir dir)
@@ -305,7 +305,7 @@ module ModPath = struct
 
   let hcons =
     Hashcons.simple_hcons HashMP.generate
-      (Dir_path.hcons,MBId.hcons,String.hcons)
+      (DirPath.hcons,MBId.hcons,String.hcons)
 
 end
 
@@ -316,7 +316,7 @@ module MPmap = Map.Make(ModPath)
 
 module KerName = struct
 
-  type t = ModPath.t * Dir_path.t * Label.t
+  type t = ModPath.t * DirPath.t * Label.t
 
   type kernel_name = t
 
@@ -328,8 +328,8 @@ module KerName = struct
 
   let to_string (mp,dir,l) =
     let dp =
-      if Dir_path.is_empty dir then "."
-      else "#" ^ Dir_path.to_string dir ^ "#"
+      if DirPath.is_empty dir then "."
+      else "#" ^ DirPath.to_string dir ^ "#"
     in
     ModPath.to_string mp ^ dp ^ Label.to_string l
 
@@ -342,7 +342,7 @@ module KerName = struct
       let c = String.compare l1 l2 in
       if not (Int.equal c 0) then c
       else
-        let c = Dir_path.compare dir1 dir2 in
+        let c = DirPath.compare dir1 dir2 in
         if not (Int.equal c 0) then c
         else ModPath.compare mp1 mp2
 
@@ -350,7 +350,7 @@ module KerName = struct
 
   module Self_Hashcons = struct
     type t = kernel_name
-    type u = (ModPath.t -> ModPath.t) * (Dir_path.t -> Dir_path.t)
+    type u = (ModPath.t -> ModPath.t) * (DirPath.t -> DirPath.t)
         * (string -> string)
     let hashcons (hmod,hdir,hstr) (mp,dir,l) =
       (hmod mp,hdir dir,hstr l)
@@ -363,7 +363,7 @@ module KerName = struct
 
   let hcons =
     Hashcons.simple_hcons HashKN.generate
-      (ModPath.hcons,Dir_path.hcons,String.hcons)
+      (ModPath.hcons,DirPath.hcons,String.hcons)
 
 end
 
@@ -479,7 +479,7 @@ let debug_pr_con cst = str (debug_string_of_con cst)
 let con_with_label cst lbl =
   let (mp1,dp1,l1) = KerName.repr (user_con cst)
   and (mp2,dp2,l2) = KerName.repr (canonical_con cst) in
-  assert (String.equal l1 l2 && Dir_path.equal dp1 dp2);
+  assert (String.equal l1 l2 && DirPath.equal dp1 dp2);
   if String.equal lbl l1
   then cst
   else make_con_equiv mp1 mp2 dp1 lbl
@@ -669,17 +669,17 @@ module Idpred = Id.Pred
 
 let name_eq = Name.equal
 
-(** Compatibility layer for [Dir_path] *)
+(** Compatibility layer for [DirPath] *)
 
-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
+type dir_path = DirPath.t
+let dir_path_ord = DirPath.compare
+let dir_path_eq = DirPath.equal
+let make_dirpath = DirPath.make
+let repr_dirpath = DirPath.repr
+let empty_dirpath = DirPath.empty
+let is_empty_dirpath = DirPath.is_empty
+let string_of_dirpath = DirPath.to_string
+let initial_dir = DirPath.initial
 
 (** Compatibility layer for [MBId] *)
 
@@ -705,7 +705,7 @@ let eq_label = Label.equal
 (** Compatibility layer for [ModPath] *)
 
 type module_path = ModPath.t =
-  | MPfile of Dir_path.t
+  | MPfile of DirPath.t
   | MPbound of MBId.t
   | MPdot of module_path * Label.t
 let check_bound_mp = ModPath.is_bound
diff --git a/kernel/names.mli b/kernel/names.mli
index 9a15a3a69..e194b3856 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -76,7 +76,7 @@ type module_ident = Id.t
 
 (** {6 Directory paths = section names paths } *)
 
-module Dir_path :
+module DirPath :
 sig
   type t
   (** Type of directory paths. Essentially a list of module identifiers. The
@@ -155,11 +155,11 @@ sig
   val compare : t -> t -> int
   (** Comparison over unique bound names. *)
 
-  val make : Dir_path.t -> Id.t -> t
+  val make : DirPath.t -> Id.t -> t
   (** The first argument is a file name, to prevent conflict between different
       files. *)
 
-  val repr : t -> int * Id.t * Dir_path.t
+  val repr : t -> int * Id.t * DirPath.t
   (** Reverse of [make]. *)
 
   val to_id : t -> Id.t
@@ -180,7 +180,7 @@ module ModIdmap : Map.S with type key = module_ident
 module ModPath :
 sig
   type t =
-    | MPfile of Dir_path.t
+    | MPfile of DirPath.t
     | MPbound of MBId.t
     | MPdot of t * Label.t
 
@@ -206,8 +206,8 @@ sig
   type t
 
   (** Constructor and destructor *)
-  val make : ModPath.t -> Dir_path.t -> Label.t -> t
-  val repr : t -> ModPath.t * Dir_path.t * Label.t
+  val make : ModPath.t -> DirPath.t -> Label.t -> t
+  val repr : t -> ModPath.t * DirPath.t * Label.t
 
   (** Projections *)
   val modpath : t -> ModPath.t
@@ -255,12 +255,12 @@ module Constrmap_env : Map.S with type key = constructor
 
 val constant_of_kn : KerName.t -> constant
 val constant_of_kn_equiv : KerName.t -> KerName.t -> constant
-val make_con : ModPath.t -> Dir_path.t -> Label.t -> constant
-val make_con_equiv : ModPath.t -> ModPath.t -> Dir_path.t
+val make_con : ModPath.t -> DirPath.t -> Label.t -> constant
+val make_con_equiv : ModPath.t -> ModPath.t -> DirPath.t
   -> Label.t -> constant
 val user_con : constant -> KerName.t
 val canonical_con : constant -> KerName.t
-val repr_con : constant -> ModPath.t * Dir_path.t * Label.t
+val repr_con : constant -> ModPath.t * DirPath.t * Label.t
 val eq_constant : constant -> constant -> bool
 val con_ord : constant -> constant -> int
 val con_user_ord : constant -> constant -> int
@@ -277,12 +277,12 @@ val debug_string_of_con : constant -> string
 
 val mind_of_kn : KerName.t -> mutual_inductive
 val mind_of_kn_equiv : KerName.t -> KerName.t -> mutual_inductive
-val make_mind : ModPath.t -> Dir_path.t -> Label.t -> mutual_inductive
-val make_mind_equiv : ModPath.t -> ModPath.t -> Dir_path.t 
+val make_mind : ModPath.t -> DirPath.t -> Label.t -> mutual_inductive
+val make_mind_equiv : ModPath.t -> ModPath.t -> DirPath.t 
   -> Label.t -> mutual_inductive
 val user_mind : mutual_inductive -> KerName.t
 val canonical_mind : mutual_inductive -> KerName.t
-val repr_mind : mutual_inductive -> ModPath.t * Dir_path.t * Label.t
+val repr_mind : mutual_inductive -> ModPath.t * DirPath.t * Label.t
 val eq_mind : mutual_inductive -> mutual_inductive -> bool
 val mind_ord : mutual_inductive -> mutual_inductive -> int
 val mind_user_ord : mutual_inductive -> mutual_inductive -> int
@@ -393,32 +393,32 @@ end
 
 (** {5 Directory paths} *)
 
-type dir_path = Dir_path.t
-(** @deprecated Alias for [Dir_path.t]. *)
+type dir_path = DirPath.t
+(** @deprecated Alias for [DirPath.t]. *)
 
 val dir_path_ord : dir_path -> dir_path -> int
-(** @deprecated Same as [Dir_path.compare]. *)
+(** @deprecated Same as [DirPath.compare]. *)
 
 val dir_path_eq : dir_path -> dir_path -> bool
-(** @deprecated Same as [Dir_path.equal]. *)
+(** @deprecated Same as [DirPath.equal]. *)
 
 val make_dirpath : module_ident list -> dir_path
-(** @deprecated Same as [Dir_path.make]. *)
+(** @deprecated Same as [DirPath.make]. *)
 
 val repr_dirpath : dir_path -> module_ident list
-(** @deprecated Same as [Dir_path.repr]. *)
+(** @deprecated Same as [DirPath.repr]. *)
 
 val empty_dirpath : dir_path
-(** @deprecated Same as [Dir_path.empty]. *)
+(** @deprecated Same as [DirPath.empty]. *)
 
 val is_empty_dirpath : dir_path -> bool
-(** @deprecated Same as [Dir_path.is_empty]. *)
+(** @deprecated Same as [DirPath.is_empty]. *)
 
 val string_of_dirpath : dir_path -> string
-(** @deprecated Same as [Dir_path.to_string]. *)
+(** @deprecated Same as [DirPath.to_string]. *)
 
-val initial_dir : Dir_path.t
-(** @deprecated Same as [Dir_path.initial]. *)
+val initial_dir : DirPath.t
+(** @deprecated Same as [DirPath.initial]. *)
 
 (** {5 Labels} *)
 
@@ -454,10 +454,10 @@ val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
 val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
 (** @deprecated Same as [MBId.equal]. *)
 
-val make_mbid : Dir_path.t -> Id.t -> mod_bound_id
+val make_mbid : DirPath.t -> Id.t -> mod_bound_id
 (** @deprecated Same as [MBId.make]. *)
 
-val repr_mbid : mod_bound_id -> int * Id.t * Dir_path.t
+val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t
 (** @deprecated Same as [MBId.repr]. *)
 
 val id_of_mbid : mod_bound_id -> Id.t
@@ -477,7 +477,7 @@ val name_eq : name -> name -> bool
 (** {5 Module paths} *)
 
 type module_path = ModPath.t =
-  | MPfile of Dir_path.t
+  | MPfile of DirPath.t
   | MPbound of MBId.t
   | MPdot of module_path * Label.t
 (** @deprecated Alias type *)
@@ -502,10 +502,10 @@ val initial_path : module_path
 type kernel_name = KerName.t
 (** @deprecated Alias type *)
 
-val make_kn : ModPath.t -> Dir_path.t -> Label.t -> kernel_name
+val make_kn : ModPath.t -> DirPath.t -> Label.t -> kernel_name
 (** @deprecated Same as [KerName.make]. *)
 
-val repr_kn : kernel_name -> module_path * Dir_path.t * Label.t
+val repr_kn : kernel_name -> module_path * DirPath.t * Label.t
 (** @deprecated Same as [KerName.repr]. *)
 
 val modpath : kernel_name -> module_path
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2e21a86ff..a591fb433 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -76,7 +76,7 @@ type modvariant =
   | NONE
   | SIG of (* funsig params *) (MBId.t * module_type_body) list
   | STRUCT of (* functor params *) (MBId.t * module_type_body) list
-  | LIBRARY of Dir_path.t
+  | LIBRARY of DirPath.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.t * Digest.t
+type library_info = DirPath.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 Dir_path.is_empty dir then hcons_const_body cb else cb
+      if DirPath.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 Dir_path.empty l in
+	   let kn = make_kn mp_sup DirPath.empty l in
 	   C (constant_of_delta_kn resolver kn)
        | SFBmind _ ->
-	   let kn = make_kn mp_sup Dir_path.empty l in
+	   let kn = make_kn mp_sup DirPath.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.t * module_body * library_info list * engagement option
+    DirPath.t * module_body * library_info list * engagement option
       * Nativecode.symbol array
 
 type native_library = Nativecode.global list
@@ -646,10 +646,10 @@ let start_library dir senv =
   if not (is_empty senv) then
     anomaly ~label:"Safe_typing.start_library" (Pp.str "environment should be empty");
   let dir_path,l =
-    match (Dir_path.repr dir) with
+    match (DirPath.repr dir) with
 	[] -> anomaly (Pp.str "Empty dirpath in Safe_typing.start_library")
       | hd::tl ->
-	  Dir_path.make tl, Label.of_id hd
+	  DirPath.make tl, Label.of_id hd
   in
   let mp = MPfile dir in
   let modinfo = {modpath = mp;
@@ -685,7 +685,7 @@ let export senv dir =
   begin
     match modinfo.variant with
       | LIBRARY dp ->
-	  if not (Dir_path.equal dir dp) then
+	  if not (DirPath.equal dir dp) then
 	    anomaly (Pp.str "We are not exporting the right library!")
       | _ ->
 	  anomaly (Pp.str "We are not exporting the library")
@@ -720,9 +720,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 "^(Dir_path.to_string id)^".")
+	  ("Inconsistent assumptions over module "^(DirPath.to_string id)^".")
     with Not_found ->
-      error ("Reference to unknown module "^(Dir_path.to_string id)^".")
+      error ("Reference to unknown module "^(DirPath.to_string id)^".")
   in
   List.iter check needed
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 7cddde954..1bb43a53e 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.t -> Label.t -> global_declaration -> safe_environment ->
+  DirPath.t -> Label.t -> global_declaration -> safe_environment ->
       constant * safe_environment
 
 (** Adding an inductive type *)
 val add_mind :
-  Dir_path.t -> Label.t -> mutual_inductive_entry -> safe_environment ->
+  DirPath.t -> Label.t -> mutual_inductive_entry -> safe_environment ->
     mutual_inductive * safe_environment
 
 (** Adding a module *)
@@ -103,10 +103,10 @@ type compiled_library
 
 type native_library = Nativecode.global list
 
-val start_library : Dir_path.t -> safe_environment
+val start_library : DirPath.t -> safe_environment
       -> module_path * safe_environment
 
-val export : safe_environment -> Dir_path.t
+val export : safe_environment -> DirPath.t
       -> module_path * compiled_library * native_library
 
 val import : compiled_library -> Digest.t -> safe_environment
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 11ae7c863..9e9d5b580 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 Dir_path.empty l in
+  let ind = make_mind mp DirPath.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 Dir_path.empty l in
-  let kn2 = make_mind mp2 Dir_path.empty l in
+  let kn1 = make_mind mp1 DirPath.empty l in
+  let kn2 = make_mind mp2 DirPath.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 9a27ff2a3..26254be23 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.t
+    | Level of int * Names.DirPath.t
 
   (* A specialized comparison function: we compare the [int] part first.
-     This way, most of the time, the [Dir_path.t] part is not considered.
+     This way, most of the time, the [DirPath.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.compare dp1 dp2)
+      else Names.DirPath.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.compare dp1 dp2) 0
+      Int.equal i1 i2 && Int.equal (Names.DirPath.compare dp1 dp2) 0
     | _ -> false
 
   let make m n = Level (n, m)
 
   let to_string = function
     | Set -> "Set"
-    | Level (n,d) -> Names.Dir_path.to_string d^"."^string_of_int n
+    | Level (n,d) -> Names.DirPath.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.Dir_path.make [Names.Id.of_string "Type"] in
+  let mp = Names.DirPath.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
@@ -838,7 +838,7 @@ let sort_universes orig =
 
 let fresh_level =
   let n = ref 0 in
-  fun () -> incr n; UniverseLevel.Level (!n, Names.Dir_path.empty)
+  fun () -> incr n; UniverseLevel.Level (!n, Names.DirPath.empty)
 
 let fresh_local_univ () = Atom (fresh_level ())
 
@@ -972,7 +972,7 @@ module Hunivlevel =
   Hashcons.Make(
     struct
       type t = universe_level
-      type u = Names.Dir_path.t -> Names.Dir_path.t
+      type u = Names.DirPath.t -> Names.DirPath.t
       let hashcons hdir = function
 	| UniverseLevel.Set -> UniverseLevel.Set
 	| UniverseLevel.Level (n,d) -> UniverseLevel.Level (n,hdir d)
@@ -1005,7 +1005,7 @@ module Huniv =
       let hash = Hashtbl.hash
     end)
 
-let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.Dir_path.hcons
+let hcons_univlevel = Hashcons.simple_hcons Hunivlevel.generate Names.DirPath.hcons
 let hcons_univ = Hashcons.simple_hcons Huniv.generate hcons_univlevel
 
 module Hconstraint =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index b466057a2..c74797c8b 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.t -> int -> t
+  val make : Names.DirPath.t -> int -> t
   (** Create a new universe level from a unique identifier and an associated
       module path. *)