From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 01:58:04 +0200 Subject: Remove errorlabstrm in favor of user_err As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch. --- checker/check.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'checker/check.ml') diff --git a/checker/check.ml b/checker/check.ml index 863cf7b2c..38d2057eb 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 - errorlabstrm "load_absolute_library_from" + user_err "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 = - errorlabstrm "load_absolute_library_from" + user_err "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 - errorlabstrm "intern_from_file" (str "Checksum mismatch"); + user_err "intern_from_file" (str "Checksum mismatch"); let () = close_in ch in if dir <> sd.md_name then - errorlabstrm "intern_from_file" + user_err "intern_from_file" (name_clash_message dir sd.md_name f); if tasks <> None || discharging <> None then - errorlabstrm "intern_from_file" + user_err "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 - errorlabstrm "intern_from_file" + user_err "intern_from_file" (str "The file "++str f++str " is still a .vio")) opaque_csts; Validate.validate !Flags.debug Values.v_univopaques opaque_csts; -- cgit v1.2.3