Merge PR #244.

4 files changed, 11 insertions, 9 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 863cf7b2cd..8565e96fc9 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 ~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 =
-  errorlabstrm "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
-        errorlabstrm "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
-        errorlabstrm "intern_from_file"
+        user_err ~hdr:"intern_from_file"
           (name_clash_message dir sd.md_name f);
       if tasks <> None || discharging <> None then
-        errorlabstrm "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
-        errorlabstrm "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;
diff --git a/checker/checker.ml b/checker/checker.ml
index 0c411ae44d..06d0cd1c03 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -213,7 +213,9 @@ let report () = (str "." ++ spc () ++ str "Please report.")
 
 let guill s = str "\"" ++ str s ++ str "\""
 
-let where s =
+let where = function
+| None -> mt ()
+| Some s ->
   if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
 let rec explain_exn = function
diff --git a/checker/modops.ml b/checker/modops.ml
index b720fb6213..aba9da2fef 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -33,7 +33,7 @@ let error_no_such_label_sub l l1 =
          Label.to_string l^" is missing in "^l1^".")
 
 let error_not_a_module_loc loc s =
-  user_err_loc (loc,"",str ("\""^Label.to_string s^"\" is not a module"))
+  user_err ~loc  (str ("\""^Label.to_string s^"\" is not a module"))
 
 let error_not_a_module s = error_not_a_module_loc Loc.ghost s
 
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 11cd742ba4..53d80c6d55 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -89,6 +89,6 @@ let import file clib univs digest =
 let unsafe_import file clib univs digest =
   let env = !genv in
   if !Flags.debug then check_imports Feedback.msg_warning clib.comp_name env clib.comp_deps
-  else check_imports (errorlabstrm"unsafe_import") clib.comp_name env clib.comp_deps;
+  else check_imports (user_err ~hdr:"unsafe_import") clib.comp_name env clib.comp_deps;
   check_engagement env clib.comp_enga;
   full_add_module clib.comp_name clib.comp_mod univs digest