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, 31 insertions, 31 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 31f75f4f9..49fe6d0ba 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -11,19 +11,19 @@ open Errors
 open Util
 open Names
 
-let pr_dirpath dp = str (string_of_dirpath dp)
-let default_root_prefix = make_dirpath []
+let pr_dirpath dp = str (Dir_path.to_string dp)
+let default_root_prefix = Dir_path.make []
 let split_dirpath d =
-  let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
-let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
+  let l = Dir_path.repr d in (Dir_path.make (List.tl l), List.hd l)
+let extend_dirpath p id = Dir_path.make (id :: Dir_path.repr p)
 
 type section_path = {
   dirpath : string list ;
   basename : string }
 let dir_of_path p =
-  make_dirpath (List.map Id.of_string p.dirpath)
+  Dir_path.make (List.map Id.of_string p.dirpath)
 let path_of_dirpath dir =
-  match repr_dirpath dir with
+  match Dir_path.repr dir with
       [] -> failwith "path_of_dirpath"
     | l::dir ->
         {dirpath=List.map Id.to_string dir;basename=Id.to_string l}
@@ -36,7 +36,7 @@ let pr_path sp =
 
 type library_objects
 
-type compilation_unit_name = dir_path
+type compilation_unit_name = Dir_path.t
 
 type library_disk = {
   md_name : compilation_unit_name;
@@ -61,10 +61,10 @@ type library_t = {
 
 module LibraryOrdered =
   struct
-    type t = dir_path
+    type t = Dir_path.t
     let compare d1 d2 =
       Pervasives.compare
-        (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+        (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2))
   end
 
 module LibrarySet = Set.Make(LibraryOrdered)
@@ -81,7 +81,7 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (string_of_dirpath dir))
+    error ("Unknown library " ^ (Dir_path.to_string dir))
 
 let library_full_filename dir = (find_library dir).library_filename
 
@@ -113,7 +113,7 @@ let check_one_lib admit (dir,m) =
 (*************************************************************************)
 (*s Load path. Mapping from physical to logical paths etc.*)
 
-type logical_path = dir_path
+type logical_path = Dir_path.t
 
 let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list)
 
diff --git a/checker/checker.ml b/checker/checker.ml
index 5a7efacf8..1b7af5178 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -36,7 +36,7 @@ let parse_dir s =
 let dirpath_of_string s =
   match parse_dir s with
       [] -> Check.default_root_prefix
-    | dir -> make_dirpath (List.map Id.of_string dir)
+    | dir -> Dir_path.make (List.map Id.of_string dir)
 let path_of_string s =
   match parse_dir s with
       [] -> invalid_arg "path_of_string"
@@ -77,11 +77,11 @@ let convert_string d =
 let add_rec_path ~unix_path ~coq_root =
   if exists_dir unix_path then
     let dirs = all_subdirs ~unix_path in
-    let prefix = repr_dirpath coq_root in
+    let prefix = Dir_path.repr coq_root in
     let convert_dirs (lp, cp) =
       try
         let path = List.map convert_string (List.rev cp) @ prefix in
-        Some (lp, Names.make_dirpath path)
+        Some (lp, Names.Dir_path.make path)
       with Exit -> None
     in
     let dirs = List.map_filter convert_dirs dirs in
@@ -113,9 +113,9 @@ let init_load_path () =
   let plugins = coqlib/"plugins" in
   (* NOTE: These directories are searched from last to first *)
   (* first standard library *)
-  add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.make_dirpath[coq_root]);
+  add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.Dir_path.make[coq_root]);
   (* then plugins *)
-  add_rec_path ~unix_path:plugins ~coq_root:(Names.make_dirpath [coq_root]);
+  add_rec_path ~unix_path:plugins ~coq_root:(Names.Dir_path.make [coq_root]);
   (* then user-contrib *)
   if Sys.file_exists user_contrib then
     add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
diff --git a/checker/environ.mli b/checker/environ.mli
index 36b76960f..0ec14cc92 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -27,8 +27,8 @@ val engagement : env -> Declarations.engagement option
 val set_engagement : Declarations.engagement -> env -> env
 
 (* Digests *)
-val add_digest : env -> dir_path -> Digest.t -> env
-val lookup_digest : env -> dir_path -> Digest.t
+val add_digest : env -> Dir_path.t -> Digest.t -> env
+val lookup_digest : env -> Dir_path.t -> Digest.t
 
 (* de Bruijn variables *)
 val rel_context : env -> rel_context
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index edd970f6b..548dd32fc 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -19,12 +19,12 @@ open Declarations
 open Environ
 
 let rec debug_string_of_mp = function
-  | MPfile sl -> string_of_dirpath sl
+  | MPfile sl -> Dir_path.to_string sl
   | MPbound uid -> "bound("^string_of_mbid uid^")"
   | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ string_of_label l
 
 let rec string_of_mp = function
-  | MPfile sl -> string_of_dirpath sl
+  | MPfile sl -> Dir_path.to_string sl
   | MPbound uid -> string_of_mbid uid
   | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7dfa29e16..b8e5fa043 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -253,10 +253,10 @@ and check_module env mp mb =
 
 and check_structure_field env mp lab res = function
   | SFBconst cb ->
-      let c = make_con mp empty_dirpath lab in
+      let c = make_con mp Dir_path.empty lab in
 	check_constant_declaration env c cb
   | SFBmind mib ->
-      let kn = make_mind mp empty_dirpath lab in
+      let kn = make_mind mp Dir_path.empty lab in
       let kn = mind_of_delta res kn in
 	Indtypes.check_inductive env kn mib
   | SFBmodule msb ->
diff --git a/checker/modops.ml b/checker/modops.ml
index 1c4a2916e..4330eff30 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -67,7 +67,7 @@ let module_body_of_type mp mtb =
 
 let rec add_signature mp sign resolver env = 
   let add_one env (l,elem) =
-    let kn = make_kn mp empty_dirpath l in
+    let kn = make_kn mp Dir_path.empty l in
     let con = constant_of_kn kn in
     let mind = mind_of_delta resolver (mind_of_kn kn) in
       match elem with
@@ -97,7 +97,7 @@ let strengthen_const mp_from l cb resolver =
   match cb.const_body with
     | Def _ -> cb
     | _ ->
-      let con = make_con mp_from empty_dirpath l in
+      let con = make_con mp_from Dir_path.empty l in
       (* let con =  constant_of_delta resolver con in*)
       { cb with const_body = Def (Declarations.from_val (Const con)) }
 
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index e5e4768a8..f0bcb3a12 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -43,9 +43,9 @@ let check_engagement env c =
 
 let report_clash f caller dir =
   let msg =
-    str "compiled library " ++ str(string_of_dirpath caller) ++
+    str "compiled library " ++ str(Dir_path.to_string caller) ++
     spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++
-    str(string_of_dirpath dir) ++ fnl() in
+    str(Dir_path.to_string dir) ++ fnl() in
   f msg
 
 
@@ -55,15 +55,15 @@ let check_imports f caller env needed =
       let actual_stamp = lookup_digest env dp in
       if stamp <> actual_stamp then report_clash f caller dp
     with Not_found ->
-      error ("Reference to unknown module " ^ (string_of_dirpath dp))
+      error ("Reference to unknown module " ^ (Dir_path.to_string dp))
   in
   List.iter check needed
 
 
 type compiled_library =
-    dir_path *
+    Dir_path.t *
     module_body *
-    (dir_path * Digest.t) list *
+    (Dir_path.t * Digest.t) list *
     engagement option
 
  (* Store the body of modules' opaque constants inside a table.  
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 390c2b9e7..951bed6c1 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -35,7 +35,7 @@ type namedmodule =
    constructors *)
 
 let add_mib_nameobjects mp l mib map =
-  let ind = make_mind mp empty_dirpath l in
+  let ind = make_mind mp Dir_path.empty l in
   let add_mip_nameobjects j oib map =
     let ip = (ind,j) in
     let map =
@@ -83,7 +83,7 @@ let check_conv_error error f env a1 a2 =
 
 (* for now we do not allow reorderings *)
 let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2= 
-  let kn = make_mind  mp1 empty_dirpath l in
+  let kn = make_mind  mp1 Dir_path.empty l in
   let error () = error_not_match l spec2 in
   let check_conv f = check_conv_error error f in
   let mib1 =