Modulification of dir_path

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

1 files changed, 11 insertions, 11 deletions

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 6ea0d09a4..23c1b2abc 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -133,8 +133,8 @@ let add_glob_gen loc sp lib_dp ty =
     let mod_dp,id = Libnames.repr_path sp in
     let mod_dp = remove_sections mod_dp in
     let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
-    let filepath = Names.string_of_dirpath lib_dp in
-    let modpath = Names.string_of_dirpath mod_dp_trunc in
+    let filepath = Names.Dir_path.to_string lib_dp in
+    let modpath = Names.Dir_path.to_string mod_dp_trunc in
     let ident = Names.Id.to_string id in
       dump_ref loc filepath modpath ident ty
 
@@ -160,12 +160,12 @@ let dump_binding loc id = ()
 let dump_definition (loc, id) sec s =
   let bl,el = interval loc in
   dump_string (Printf.sprintf "%s %d:%d %s %s\n" s bl el
-			(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.Id.to_string id))
+			(Names.Dir_path.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id))
 
 let dump_reference loc modpath ident ty =
   let bl,el = interval loc in
   dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
-		  bl el (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
+		  bl el (Names.Dir_path.to_string (Lib.library_dp ())) modpath ident ty)
 
 let dump_constraint ((loc, n), _, _) sec ty =
   match n with
@@ -176,8 +176,8 @@ let dump_modref loc mp ty =
   if dump () then
     let (dp, l) = Lib.split_modpath mp in
     let l = if List.is_empty l then l else List.drop_last l in
-    let fp = Names.string_of_dirpath dp in
-    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
+    let fp = Names.Dir_path.to_string dp in
+    let mp = Names.Dir_path.to_string (Names.Dir_path.make l) in
     let bl,el = interval loc in
       dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
 		      bl el fp mp "<>" ty)
@@ -186,13 +186,13 @@ let dump_moddef loc mp ty =
   if dump () then
     let bl,el = interval loc in
     let (dp, l) = Lib.split_modpath mp in
-    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
+    let mp = Names.Dir_path.to_string (Names.Dir_path.make l) in
       dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el "<>" mp)
 
 let dump_libref loc dp ty =
   let bl,el = interval loc in
   dump_string (Printf.sprintf "R%d:%d %s <> <> %s\n"
-		  bl el (Names.string_of_dirpath dp) ty)
+		  bl el (Names.Dir_path.to_string dp) ty)
 
 let cook_notation df sc =
   (* We encode notations so that they are space-free and still human-readable *)
@@ -234,12 +234,12 @@ let cook_notation df sc =
 let dump_notation (loc,(df,_)) sc sec =
   (* We dump the location of the opening '"' *)
   dump_string (Printf.sprintf "not %d %s %s\n" (fst (Loc.unloc loc))
-    (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc))
+    (Names.Dir_path.to_string (Lib.current_dirpath sec)) (cook_notation df sc))
 
 let dump_notation_location posl df (((path,secpath),_),sc) =
   if dump () then
-    let path = Names.string_of_dirpath path in
-    let secpath = Names.string_of_dirpath secpath in
+    let path = Names.Dir_path.to_string path in
+    let secpath = Names.Dir_path.to_string secpath in
     let df = cook_notation df sc in
     List.iter (fun (bl,el) ->
       dump_string(Printf.sprintf "R%d:%d %s %s %s not\n" bl el path secpath df))