Modulification of dir_path

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

8 files changed, 25 insertions, 25 deletions

diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 6cb97fd60..0e4d0c651 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -171,7 +171,7 @@ val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -
 val is_global : Id.t -> bool
 val construct_reference : named_context -> Id.t -> constr
 val global_reference : Id.t -> constr
-val global_reference_in_absolute_module : dir_path -> Id.t -> constr
+val global_reference_in_absolute_module : Dir_path.t -> Id.t -> constr
 
 (** Interprets a term as the left-hand side of a notation; the boolean
     list is a set and this set is [true] for a variable occurring in
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 4b2ca2004..a047a762b 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -21,7 +21,7 @@ open Smartlocate
 
 type message = string
 
-let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l))
 
 let find_reference locstr dir s =
   let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
@@ -64,10 +64,10 @@ let gen_constant_in_modules locstr dirs s =
 
 let check_required_library d =
   let d' = List.map Id.of_string d in
-  let dir = make_dirpath (List.rev d') in
+  let dir = Dir_path.make (List.rev d') in
   let mp = (fst(Lib.current_prefix())) in
   let current_dir = match mp with
-    | MPfile dp -> dir_path_eq dir dp
+    | MPfile dp -> Dir_path.equal dir dp
     | _ -> false
   in
   if not (Library.library_is_loaded dir) then
@@ -75,10 +75,10 @@ let check_required_library d =
 (* Loading silently ...
     let m, prefix = List.sep_last d' in
     read_library
-     (Loc.ghost,make_qualid (make_dirpath (List.rev prefix)) m)
+     (Loc.ghost,make_qualid (Dir_path.make (List.rev prefix)) m)
 *)
 (* or failing ...*)
-      error ("Library "^(string_of_dirpath dir)^" has to be required first.")
+      error ("Library "^(Dir_path.to_string dir)^" has to be required first.")
 
 (************************************************************************)
 (* Specific Coq objects *)
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 33392da0e..02174c876 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -54,8 +54,8 @@ val check_required_library : string list -> unit
 (** {6 Global references } *)
 
 (** Modules *)
-val logic_module : dir_path
-val logic_type_module : dir_path
+val logic_module : Dir_path.t
+val logic_type_module : Dir_path.t
 
 val datatypes_module_name : string list
 val logic_module_name : string list
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))
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 4a0752a3a..7674322c3 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -29,7 +29,7 @@ val dump_definition : Loc.t * Names.Id.t -> bool -> string -> unit
 val dump_moddef : Loc.t -> Names.module_path -> string -> unit
 val dump_modref  : Loc.t -> Names.module_path -> string -> unit
 val dump_reference  : Loc.t -> string -> string -> string -> unit
-val dump_libref : Loc.t -> Names.dir_path -> string -> unit
+val dump_libref : Loc.t -> Names.Dir_path.t -> string -> unit
 val dump_notation_location : (int * int) list -> Constrexpr.notation ->
   (Notation.notation_location * Notation_term.scope_name option) -> unit
 val dump_binding : Loc.t -> Names.Id.Set.elt -> unit
diff --git a/interp/notation.ml b/interp/notation.ml
index d5aa59788..39a664a64 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -44,14 +44,14 @@ open Ppextend
 
 type level = precedence * tolerability list
 type delimiters = string
-type notation_location = (dir_path * dir_path) * string
+type notation_location = (Dir_path.t * Dir_path.t) * string
 
 type scope = {
   notations: (string, interpretation * notation_location) Gmap.t;
   delimiters: delimiters option
 }
 
-(* Uninterpreted notation map: notation -> level * dir_path *)
+(* Uninterpreted notation map: notation -> level * Dir_path.t *)
 let notation_level_map = ref Gmap.empty
 
 (* Scopes table: scope_name -> symbol_interpretation *)
@@ -397,7 +397,7 @@ let find_prim_token g loc p sc =
   (* Try for a primitive numerical notation *)
   let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
   check_required_module loc sc spdir;
-  g (interp ()), ((dirpath (fst spdir),empty_dirpath),"")
+  g (interp ()), ((dirpath (fst spdir),Dir_path.empty),"")
 
 let interp_prim_token_gen g loc p local_scopes =
   let scopes = make_current_scopes local_scopes in
diff --git a/interp/notation.mli b/interp/notation.mli
index c3106f5d3..8b2d8aa0f 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -65,7 +65,7 @@ val find_delimiters_scope : Loc.t -> delimiters -> scope_name
    negative numbers are not supported, the interpreter must fail with
    an appropriate error message *)
 
-type notation_location = (dir_path * dir_path) * string
+type notation_location = (Dir_path.t * Dir_path.t) * string
 type required_module = full_path * string list
 type cases_pattern_status = bool (** true = use prim token in patterns *)
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 254805f6a..a07b6aa69 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -42,7 +42,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
 let is_alias_of_already_visible_name sp = function
   | _,NRef ref ->
       let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in
-      dir_path_eq dir empty_dirpath && Id.equal id (basename sp)
+      Dir_path.equal dir Dir_path.empty && Id.equal id (basename sp)
   | _ ->
       false