Merge PR #244.

2 files changed, 9 insertions, 9 deletions

diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 6149e3a114..2ab3b9c59c 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -224,7 +224,7 @@ let compute_proof_name locality = function
       if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
 	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
       then
-        user_err_loc (loc,"",pr_id id ++ str " already exists.");
+        user_err ~loc  (pr_id id ++ str " already exists.");
       id, pl
   | None ->
       next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
@@ -337,7 +337,7 @@ let get_proof proof do_guard hook opacity =
 let check_exist =
   List.iter (fun (loc,id) ->
     if not (Nametab.exists_cci (Lib.make_path id)) then
-        user_err_loc (loc,"",pr_id id ++ str " does not exist.")
+        user_err ~loc  (pr_id id ++ str " does not exist.")
   )
 
 let universe_proof_terminator compute_guard hook =
diff --git a/stm/stm.ml b/stm/stm.ml
index cf9fa54922..482bbe4c2a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1038,7 +1038,7 @@ end = struct (* {{{ *)
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
-       CErrors.errorlabstrm "undo_vernac_classifier"
+       CErrors.user_err ~hdr:"undo_vernac_classifier"
         (str "Cannot undo")
 
 end (* }}} *)
@@ -1106,7 +1106,7 @@ let proof_block_delimiters = ref []
 
 let register_proof_block_delimiter name static dynamic =
   if List.mem_assoc name !proof_block_delimiters then
-    CErrors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name);
+    CErrors.user_err ~hdr:"STM" (str "Duplicate block delimiter " ++ str name);
   proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
 
 let mk_doc_node id = function
@@ -1141,7 +1141,7 @@ let detect_proof_block id name =
           VCS.create_proof_block decl name
       end
     with Not_found ->
-      CErrors.errorlabstrm "STM"
+      CErrors.user_err ~hdr:"STM"
         (str "Unknown proof block delimiter " ++ str name)
   )
 (****************************** THE SCHEDULER *********************************)
@@ -1706,7 +1706,7 @@ end = struct (* {{{ *)
          List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
                       Evd.(evar_context g))
        then
-         CErrors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^
+         CErrors.user_err ~hdr:"STM" (strbrk("the par: goal selector supports ground "^
            "goals only"))
        else begin
         let (i, ast) = r_ast in
@@ -1719,7 +1719,7 @@ end = struct (* {{{ *)
             let t = Evarutil.nf_evar sigma t in
             if Evarutil.is_ground_term sigma t then
               RespBuiltSubProof (t, Evd.evar_universe_context sigma)
-            else CErrors.errorlabstrm "STM" (str"The solution is not ground")
+            else CErrors.user_err ~hdr:"STM" (str"The solution is not ground")
        end) ()
     with e when CErrors.noncritical e -> RespError (CErrors.print e)
 
@@ -2056,7 +2056,7 @@ let known_state ?(redefine_qed=false) ~cache id =
            | _ -> assert false
         end
       with Not_found ->
-          CErrors.errorlabstrm "STM"
+          CErrors.user_err ~hdr:"STM"
             (str "Unknown proof block delimiter " ++ str name)
   in
 
@@ -2405,7 +2405,7 @@ let handle_failure (e, info) vcs tty =
 let snapshot_vio ldir long_f_dot_vo =
   finish ();
   if List.length (VCS.branches ()) > 1 then
-    CErrors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
+    CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
   Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
     (Global.opaque_tables ())