Merge PR #244.

1 files changed, 18 insertions, 18 deletions

diff --git a/library/library.ml b/library/library.ml
index d44f796a7..3086e3d18 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -131,7 +131,7 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    errorlabstrm "Library.find_library"
+    user_err ~hdr:"Library.find_library"
       (str "Unknown library " ++ pr_dirpath dir)
 
 let register_library_filename dir f =
@@ -329,12 +329,12 @@ let locate_qualified_library ?root ?(warn = true) qid =
 
 let error_unmapped_dir qid =
   let prefix, _ = repr_qualid qid in
-  errorlabstrm "load_absolute_library_from"
+  user_err ~hdr:"load_absolute_library_from"
     (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
      str "no physical path bound to" ++ spc () ++ pr_dirpath 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_qualid qid ++ str" in loadpath")
 
 let try_locate_absolute_library dir =
@@ -378,7 +378,7 @@ let access_table what tables dp i =
       let t =
         try fetch_delayed f
         with Faulty f ->
-          errorlabstrm "Library.access_table"
+          user_err ~hdr:"Library.access_table"
             (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
              str ") is inaccessible or corrupted,\ncannot load some " ++
              str what ++ str " in it.\n")
@@ -463,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from =
   let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
   let m = intern_from_file f in
   if not (DirPath.equal dir m.library_name) then
-    errorlabstrm "load_physical_library"
+    user_err ~hdr:"load_physical_library"
       (str "The file " ++ str f ++ str " contains library" ++ spc () ++
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
@@ -477,7 +477,7 @@ and intern_library_deps libs dir m from =
 and intern_mandatory_library caller from libs (dir,d) =
   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 ++
+    user_err (str "Compiled library " ++ pr_dirpath caller ++
     str " (in file " ++ str from ++ str ") makes inconsistent assumptions \
     over library " ++ pr_dirpath dir);
   libs
@@ -582,8 +582,8 @@ let require_library_from_dirpath modrefl export =
 let safe_locate_module (loc,qid) =
   try Nametab.locate_module qid
   with Not_found ->
-    user_err_loc
-      (loc,"import_library", pr_qualid qid ++ str " is not a module")
+    user_err ~loc ~hdr:"import_library"
+      (pr_qualid qid ++ str " is not a module")
 
 let import_module export modl =
   (* Optimization: libraries in a raw in the list are imported
@@ -607,8 +607,8 @@ let import_module export modl =
             flush acc;
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
-              user_err_loc (loc,"import_library",
-                pr_qualid dir ++ str " is not a module"))
+              user_err ~loc ~hdr:"import_library"
+                (pr_qualid dir ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
@@ -619,7 +619,7 @@ let check_coq_overwriting p id =
   let l = DirPath.repr p in
   let is_empty = match l with [] -> true | _ -> false in
   if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then
-    errorlabstrm ""
+    user_err 
       (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++
       str "it starts with prefix \"Coq\" which is reserved for the Coq library.")
 
@@ -632,7 +632,7 @@ let check_module_name s =
     (if c = '\'' then str "\"'\"" else (str "'" ++ str (String.make 1 c) ++ str "'")) ++
     strbrk " is not allowed in module names\n"
   in
-  let err c = errorlabstrm "" (msg c) in
+  let err c = user_err  (msg c) in
   match String.get s 0 with
     | 'a' .. 'z' | 'A' .. 'Z' ->
         for i = 1 to (String.length s)-1 do
@@ -668,10 +668,10 @@ let load_library_todo f =
   let tasks, _, _ = System.marshal_in_segment f ch in
   let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
   close_in ch;
-  if tasks = None then errorlabstrm "restart" (str"not a .vio file");
-  if s2 = None then errorlabstrm "restart" (str"not a .vio file");
-  if s3 = None then errorlabstrm "restart" (str"not a .vio file");
-  if pi3 (Option.get s2) then errorlabstrm "restart" (str"not a .vio file");
+  if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
+  if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
+  if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
+  if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
   longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
@@ -687,7 +687,7 @@ let current_deps () =
 let current_reexports () = !libraries_exports_list
 
 let error_recursively_dependent_library dir =
-  errorlabstrm ""
+  user_err 
     (strbrk "Unable to use logical name " ++ pr_dirpath dir ++
      strbrk " to save current library because" ++
      strbrk " it already depends on a library of this name.")
@@ -734,7 +734,7 @@ let save_library_to ?todo dir f otab =
       except Int.Set.empty in
   let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
   Array.iteri (fun i x ->
-    if not(is_done_or_todo i x) then CErrors.errorlabstrm "library"
+    if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library"
       Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
     opaque_table;
   let sd = {