aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/check.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-19 20:27:51 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-02-19 20:27:51 +0000
commit248728628f5da946f96c22ba0a0e7e9b33019382 (patch)
tree905dbbafa65dd7bf02823318326be2ca389f833f /checker/check.ml
parent3889c9a9e7d017ef2eea647d8c17d153a0b90083 (diff)
Dir_path --> DirPath
Ok, this is merely a matter of taste, but up to now the usage in Coq is rather to use capital letters instead of _ in the names of inner modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 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 4c4ba980d..c3f0e976f 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -11,19 +11,19 @@ open Errors
open Util
open Names
-let pr_dirpath dp = str (Dir_path.to_string dp)
-let default_root_prefix = Dir_path.empty
+let pr_dirpath dp = str (DirPath.to_string dp)
+let default_root_prefix = DirPath.empty
let split_dirpath d =
- 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)
+ let l = DirPath.repr d in (DirPath.make (List.tl l), List.hd l)
+let extend_dirpath p id = DirPath.make (id :: DirPath.repr p)
type section_path = {
dirpath : string list ;
basename : string }
let dir_of_path p =
- Dir_path.make (List.map Id.of_string p.dirpath)
+ DirPath.make (List.map Id.of_string p.dirpath)
let path_of_dirpath dir =
- match Dir_path.repr dir with
+ match DirPath.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.t
+type compilation_unit_name = DirPath.t
type library_disk = {
md_name : compilation_unit_name;
@@ -61,10 +61,10 @@ type library_t = {
module LibraryOrdered =
struct
- type t = Dir_path.t
+ type t = DirPath.t
let compare d1 d2 =
Pervasives.compare
- (List.rev (Dir_path.repr d1)) (List.rev (Dir_path.repr d2))
+ (List.rev (DirPath.repr d1)) (List.rev (DirPath.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 " ^ (Dir_path.to_string dir))
+ error ("Unknown library " ^ (DirPath.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.t
+type logical_path = DirPath.t
let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list)