aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/check.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-14 15:57:08 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-14 15:57:08 +0000
commitf42dd8d8530e6227621ccd662741f1da23700304 (patch)
tree1838306cdafaa8486ec792c1ab48b64162e027c9 /checker/check.ml
parent67f5c70a480c95cfb819fc68439781b5e5e95794 (diff)
Modulification of dir_path
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/check.ml')
-rw-r--r--checker/check.ml22
1 files changed, 11 insertions, 11 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)