Modulification of dir_path

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

3 files changed, 11 insertions, 11 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index dee144b951..3a5cb784e6 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 44c2466616..7ee5b92def 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 b83d97f6a1..afd4d37f36 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