Merge PR #244.

1 files changed, 6 insertions, 6 deletions

diff --git a/library/lib.ml b/library/lib.ml
index a5a9a0194..749cc4ff3 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -78,7 +78,7 @@ let classify_segment seg =
     | (_,ClosedModule _) :: stk -> clean acc stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
     | (_,OpenedModule (ty,_,_,_)) :: _ ->
-      errorlabstrm "Lib.classify_segment"
+      user_err ~hdr:"Lib.classify_segment"
         (str "there are still opened " ++ str (module_kind ty) ++ str "s")
     | (_,FrozenState _) :: stk -> clean acc stk
   in
@@ -270,7 +270,7 @@ let start_mod is_type export id mp fs =
     else Nametab.exists_module dir
   in
   if exists then
-    errorlabstrm "open_module" (pr_id id ++ str " already exists");
+    user_err ~hdr:"open_module" (pr_id id ++ str " already exists");
   add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
   path_prefix := prefix;
   prefix
@@ -280,7 +280,7 @@ let start_modtype = start_mod true None
 
 let error_still_opened string oname =
   let id = basename (fst oname) in
-  errorlabstrm ""
+  user_err 
     (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.")
 
 let end_mod is_type =
@@ -325,7 +325,7 @@ let end_compilation_checks dir =
     try match snd (find_entry_p is_opening_node) with
       | OpenedSection _ -> error "There are some open sections."
       | OpenedModule (ty,_,_,_) ->
-	errorlabstrm "Lib.end_compilation_checks"
+	user_err ~hdr:"Lib.end_compilation_checks"
           (str "There are some open " ++ str (module_kind ty) ++ str "s.")
       | _ -> assert false
     with Not_found -> ()
@@ -377,7 +377,7 @@ let find_opening_node id =
     let oname,entry = find_entry_p is_opening_node in
     let id' = basename (fst oname) in
     if not (Names.Id.equal id id') then
-      errorlabstrm "Lib.find_opening_node"
+      user_err ~hdr:"Lib.find_opening_node"
         (str "Last block to end has name " ++ pr_id id' ++ str ".");
     entry
   with Not_found -> error "There is nothing to end."
@@ -520,7 +520,7 @@ let open_section id =
   let dir = add_dirpath_suffix olddir id in
   let prefix = dir, (mp, add_dirpath_suffix oldsec id) in
   if Nametab.exists_section dir then
-    errorlabstrm "open_section" (pr_id id ++ str " already exists.");
+    user_err ~hdr:"open_section" (pr_id id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:`No in
   add_entry (make_oname id) (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)