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

1 files changed, 30 insertions, 30 deletions

diff --git a/library/libnames.ml b/library/libnames.ml
index 9f129793e..43ece3417 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -13,38 +13,38 @@ open Names
 
 (**********************************************)
 
-let pr_dirpath sl = (str (Dir_path.to_string sl))
+let pr_dirpath sl = (str (DirPath.to_string sl))
 
 (*s Operations on dirpaths *)
 
 (* Pop the last n module idents *)
 let pop_dirpath_n n dir =
-  Dir_path.make (List.skipn n (Dir_path.repr dir))
+  DirPath.make (List.skipn n (DirPath.repr dir))
 
-let pop_dirpath p = match Dir_path.repr p with
+let pop_dirpath p = match DirPath.repr p with
   | [] -> anomaly (str "dirpath_prefix: empty dirpath")
-  | _::l -> Dir_path.make l
+  | _::l -> DirPath.make l
 
 let is_dirpath_prefix_of d1 d2 =
-  List.prefix_of (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2))
+  List.prefix_of (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
 
 let chop_dirpath n d =
-  let d1,d2 = List.chop n (List.rev (Dir_path.repr d)) in
-    Dir_path.make (List.rev d1), Dir_path.make (List.rev d2)
+  let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in
+    DirPath.make (List.rev d1), DirPath.make (List.rev d2)
 
 let drop_dirpath_prefix d1 d2 =
-  let d = Util.List.drop_prefix (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2)) in
-    Dir_path.make (List.rev d)
+  let d = Util.List.drop_prefix (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) in
+    DirPath.make (List.rev d)
 
-let append_dirpath d1 d2 = Dir_path.make (Dir_path.repr d2 @ Dir_path.repr d1)
+let append_dirpath d1 d2 = DirPath.make (DirPath.repr d2 @ DirPath.repr d1)
 
 (* To know how qualified a name should be to be understood in the current env*)
-let add_dirpath_prefix id d = Dir_path.make (Dir_path.repr d @ [id])
+let add_dirpath_prefix id d = DirPath.make (DirPath.repr d @ [id])
 
 let split_dirpath d =
-  let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l)
+  let l = DirPath.repr d in (DirPath.make (List.tl l), List.hd l)
 
-let add_dirpath_suffix p id = Dir_path.make (id :: Dir_path.repr p)
+let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p)
 
 (* parsing *)
 let parse_dir s =
@@ -68,22 +68,22 @@ let dirpath_of_string s =
   | "" -> []
   | _ -> parse_dir s
   in
-  Dir_path.make path
+  DirPath.make path
 
-let string_of_dirpath = Names.Dir_path.to_string
+let string_of_dirpath = Names.DirPath.to_string
 
-module Dirset = Set.Make(struct type t = Dir_path.t let compare = Dir_path.compare end)
-module Dirmap = Map.Make(struct type t = Dir_path.t let compare = Dir_path.compare end)
+module Dirset = Set.Make(struct type t = DirPath.t let compare = DirPath.compare end)
+module Dirmap = Map.Make(struct type t = DirPath.t let compare = DirPath.compare end)
 
 (*s Section paths are absolute names *)
 
 type full_path = {
-  dirpath : Dir_path.t ;
+  dirpath : DirPath.t ;
   basename : Id.t }
 
 let eq_full_path p1 p2 =
   Id.equal p1.basename p2.basename &&
-  Dir_path.equal p1.dirpath p2.dirpath
+  DirPath.equal p1.dirpath p2.dirpath
 
 let make_path pa id = { dirpath = pa; basename = id }
 
@@ -92,9 +92,9 @@ let repr_path { dirpath = pa; basename = id } = (pa,id)
 (* parsing and printing of section paths *)
 let string_of_path sp =
   let (sl,id) = repr_path sp in
-  match Dir_path.repr sl with
+  match DirPath.repr sl with
   | [] -> Id.to_string id
-  | _ -> (Dir_path.to_string sl) ^ "." ^ (Id.to_string id)
+  | _ -> (DirPath.to_string sl) ^ "." ^ (Id.to_string id)
 
 let sp_ord sp1 sp2 =
   let (p1,id1) = repr_path sp1
@@ -124,8 +124,8 @@ let pr_path sp = str (string_of_path sp)
 
 let restrict_path n sp =
   let dir, s = repr_path sp in
-  let dir' = List.firstn n (Dir_path.repr dir) in
-  make_path (Dir_path.make dir') s
+  let dir' = List.firstn n (DirPath.repr dir) in
+  make_path (DirPath.make dir') s
 
 (*s qualified names *)
 type qualid = full_path
@@ -141,30 +141,30 @@ let pr_qualid = pr_path
 let qualid_of_string = path_of_string
 
 let qualid_of_path sp = sp
-let qualid_of_ident id = make_qualid Dir_path.empty id
+let qualid_of_ident id = make_qualid DirPath.empty id
 let qualid_of_dirpath dir =
   let (l,a) = split_dirpath dir in
   make_qualid l a
 
 type object_name = full_path * kernel_name
 
-type object_prefix = Dir_path.t * (module_path * Dir_path.t)
+type object_prefix = DirPath.t * (module_path * DirPath.t)
 
 let make_oname (dirpath,(mp,dir)) id =
   make_path dirpath id, make_kn mp dir (Label.of_id id)
 
-(* to this type are mapped Dir_path.t's in the nametab *)
+(* to this type are mapped DirPath.t's in the nametab *)
 type global_dir_reference =
   | DirOpenModule of object_prefix
   | DirOpenModtype of object_prefix
   | DirOpenSection of object_prefix
   | DirModule of object_prefix
-  | DirClosedSection of Dir_path.t
+  | DirClosedSection of DirPath.t
       (* this won't last long I hope! *)
 
 let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) =
-  Dir_path.equal d1 d2 &&
-  Dir_path.equal p1 p2 &&
+  DirPath.equal d1 d2 &&
+  DirPath.equal p1 p2 &&
   mp_eq mp1 mp2
 
 let eq_global_dir_reference r1 r2 = match r1, r2 with
@@ -172,7 +172,7 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
 | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
 | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
 | DirModule op1, DirModule op2 -> eq_op op1 op2
-| DirClosedSection dp1, DirClosedSection dp2 -> Dir_path.equal dp1 dp2
+| DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2
 | _ -> false
 
 type reference =