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

3 files changed, 11 insertions, 11 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 0264f67fa..732903af9 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_path.is_empty dir then
+	if DirPath.is_empty dir 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 not (Dir_path.is_empty dir) then raise Not_found;
+    if not (DirPath.is_empty 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 c9341eead..0b8393d52 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 = Dir_path.make [id] in
+    let dir = DirPath.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 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)));
+  let fp = Libnames.make_path DirPath.empty id in
+  let dir = DirPath.make [id] in
+  Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.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 (Label.to_id l) (ConstRef (make_con mp Dir_path.empty l))
+      push (Label.to_id l) (ConstRef (make_con mp DirPath.empty l))
     | SFBmind mib ->
-      let mind = make_mind mp Dir_path.empty l in
+      let mind = make_mind mp DirPath.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 Dir_path.empty l) mib
+	Printer.pr_mutual_inductive_body env (make_mind mp DirPath.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_path.is_empty dir ||
+    DirPath.is_empty dir ||
     try
       match Nametab.locate_dir (qualid_of_dirpath dir) with
 	  DirOpenModtype _ -> false
diff --git a/printing/printmod.mli b/printing/printmod.mli
index afd4d37f3..1e6d1f4ce 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.t -> bool
+val printable_body : DirPath.t -> bool
 
 val print_module : bool -> module_path -> Pp.std_ppcmds