diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-28 19:52:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-08-28 19:55:54 +0200 |
| commit | 812712c0683d03760c10ef7397fb4ff0041c4860 (patch) | |
| tree | 0771a38df6d4118ee10678543667e3d156b47b7c /library/library.ml | |
| parent | 2b4517cf85432d68e53ac46815309fd8068a40ad (diff) | |
Fix bug #4750: Change format of inconsistent assumptions message.
We now print the file responsible for the incompatibility in require error
messages.
Diffstat (limited to 'library/library.ml')
| -rw-r--r-- | library/library.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/library/library.ml b/library/library.ml index 12090183a..04b82f2f3 100644 --- a/library/library.ml +++ b/library/library.ml @@ -468,16 +468,18 @@ let rec intern_library (needed, contents) (dir, f) from = pr_dirpath m.library_name ++ spc () ++ str "and not library" ++ spc() ++ pr_dirpath dir); Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); - m.library_digests, intern_library_deps (needed, contents) dir m (Some f) + m.library_digests, intern_library_deps (needed, contents) dir m f and intern_library_deps libs dir m from = let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in (dir :: needed, DPMap.add dir m contents ) and intern_mandatory_library caller from libs (dir,d) = - let digest, libs = intern_library libs (dir, None) from in + let digest, libs = intern_library libs (dir, None) (Some from) in if not (Safe_typing.digest_match ~actual:digest ~required:d) then - errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir); + errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ + str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ + over library " ++ pr_dirpath dir); libs let rec_intern_library libs (dir, f) = |