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/safe_typing.ml | |
| 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/safe_typing.ml')
| -rw-r--r-- | checker/safe_typing.ml | 10 |
1 files changed, 5 insertions, 5 deletions
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. |