diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-02-19 20:27:51 +0000 |
commit | 248728628f5da946f96c22ba0a0e7e9b33019382 (patch) | |
tree | 905dbbafa65dd7bf02823318326be2ca389f833f /checker | |
parent | 3889c9a9e7d017ef2eea647d8c17d153a0b90083 (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')
-rw-r--r-- | checker/check.ml | 22 | ||||
-rw-r--r-- | checker/checker.ml | 10 | ||||
-rw-r--r-- | checker/environ.mli | 4 | ||||
-rw-r--r-- | checker/indtypes.ml | 4 | ||||
-rw-r--r-- | checker/mod_checking.ml | 4 | ||||
-rw-r--r-- | checker/modops.ml | 4 | ||||
-rw-r--r-- | checker/safe_typing.ml | 10 | ||||
-rw-r--r-- | checker/subtyping.ml | 4 |
8 files changed, 31 insertions, 31 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) diff --git a/checker/checker.ml b/checker/checker.ml index 5cfd71fbf..9834b1331 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 -> Dir_path.make (List.map Id.of_string dir) + | dir -> DirPath.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 = Dir_path.repr coq_root in + let prefix = DirPath.repr coq_root in let convert_dirs (lp, cp) = try let path = List.rev_map convert_string cp @ prefix in - Some (lp, Names.Dir_path.make path) + Some (lp, Names.DirPath.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.Dir_path.make[coq_root]); + add_rec_path ~unix_path:(coqlib/"theories") ~coq_root:(Names.DirPath.make[coq_root]); (* then plugins *) - add_rec_path ~unix_path:plugins ~coq_root:(Names.Dir_path.make [coq_root]); + add_rec_path ~unix_path:plugins ~coq_root:(Names.DirPath.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 0ec14cc92..095d93ae5 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.t -> Digest.t -> env -val lookup_digest : env -> Dir_path.t -> Digest.t +val add_digest : env -> DirPath.t -> Digest.t -> env +val lookup_digest : env -> DirPath.t -> Digest.t (* de Bruijn variables *) val rel_context : env -> rel_context diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 8b56b5365..9a669e403 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 -> Dir_path.to_string sl + | MPfile sl -> DirPath.to_string sl | MPbound uid -> "bound("^MBId.to_string uid^")" | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ Label.to_string l let rec string_of_mp = function - | MPfile sl -> Dir_path.to_string sl + | MPfile sl -> DirPath.to_string sl | MPbound uid -> MBId.to_string uid | MPdot (mp,l) -> string_of_mp mp ^ "." ^ Label.to_string l diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index abc2da8b6..169fa5ca8 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -258,10 +258,10 @@ and check_module env mp mb = and check_structure_field env mp lab res = function | SFBconst cb -> - let c = make_con mp Dir_path.empty lab in + let c = make_con mp DirPath.empty lab in check_constant_declaration env c cb | SFBmind mib -> - let kn = make_mind mp Dir_path.empty lab in + let kn = make_mind mp DirPath.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 6b7a9c7a1..38cd09956 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 Dir_path.empty l in + let kn = make_kn mp DirPath.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 Dir_path.empty l in + let con = make_con mp_from DirPath.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 f0bcb3a12..5a190de7f 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(Dir_path.to_string caller) ++ + str "compiled library " ++ str(DirPath.to_string caller) ++ spc() ++ str "makes inconsistent assumptions over library" ++ spc() ++ - str(Dir_path.to_string dir) ++ fnl() in + str(DirPath.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 " ^ (Dir_path.to_string dp)) + error ("Reference to unknown module " ^ (DirPath.to_string dp)) in List.iter check needed type compiled_library = - Dir_path.t * + DirPath.t * module_body * - (Dir_path.t * Digest.t) list * + (DirPath.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 b23043a37..02006a7ac 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 Dir_path.empty l in + let ind = make_mind mp DirPath.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 Dir_path.empty l in + let kn = make_mind mp1 DirPath.empty l in let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in let mib1 = |