aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/check.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-08-19 02:35:47 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2016-08-19 02:46:38 +0200
commitfc579fdc83b751a44a18d2373e86ab38806e7306 (patch)
treeb325c2ff65c505ad62ac7b3fce6bce28633a60f0 /checker/check.ml
parent543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (diff)
Make the user_err header an optional parameter.
Suggested by @ppedrot
Diffstat (limited to 'checker/check.ml')
-rw-r--r--checker/check.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 38d2057eb..8565e96fc 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -247,12 +247,12 @@ let locate_qualified_library qid =
let error_unmapped_dir qid =
let prefix = qid.dirpath in
- user_err "load_absolute_library_from"
+ user_err ~hdr:"load_absolute_library_from"
(str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
let error_lib_not_found qid =
- user_err "load_absolute_library_from"
+ user_err ~hdr:"load_absolute_library_from"
(str"Cannot find library " ++ pr_path qid ++ str" in loadpath")
let try_locate_absolute_library dir =
@@ -313,18 +313,18 @@ let intern_from_file (dir, f) =
let () = close_in ch in
let ch = open_in_bin f in
if not (String.equal (Digest.channel ch pos) checksum) then
- user_err "intern_from_file" (str "Checksum mismatch");
+ user_err ~hdr:"intern_from_file" (str "Checksum mismatch");
let () = close_in ch in
if dir <> sd.md_name then
- user_err "intern_from_file"
+ user_err ~hdr:"intern_from_file"
(name_clash_message dir sd.md_name f);
if tasks <> None || discharging <> None then
- user_err "intern_from_file"
+ user_err ~hdr:"intern_from_file"
(str "The file "++str f++str " contains unfinished tasks");
if opaque_csts <> None then begin
Feedback.msg_notice(str " (was a vio file) ");
Option.iter (fun (_,_,b) -> if not b then
- user_err "intern_from_file"
+ user_err ~hdr:"intern_from_file"
(str "The file "++str f++str " is still a .vio"))
opaque_csts;
Validate.validate !Flags.debug Values.v_univopaques opaque_csts;