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.
author: Emilio Jesus Gallego Arias <e+git@x80.org> 2016-08-19 01:58:04 +0200
committer: Emilio Jesus Gallego Arias <e+git@x80.org> 2016-08-19 02:01:56 +0200
commit: 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (patch)
tree: caf22d0e607ed9e0bf9ba64d76b4c2aebce63d5a
parent: de038270f72214b169d056642eb7144a79e6f126 (diff)
85 files changed, 281 insertions, 274 deletions
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;
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 11cd742ba..c0b3a3e73 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"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
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index ac874befd..699130944 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -2,11 +2,15 @@
 = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
 =========================================
 
+* ML API *
+
 ** Error handling **
 
-All error functions now take an optional parameter `?loc:Loc.t`. For
-functions that used to carry a suffix `_loc`, such suffix has been
-dropped.
+- All error functions now take an optional parameter `?loc:Loc.t`. For
+  functions that used to carry a suffix `_loc`, such suffix has been
+  dropped.
+
+- `errorlabstrm` has been removed in favor of `user_err`.
 
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index 3e2988676..797b0aded 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -1012,7 +1012,7 @@ the different kinds of errors used in \Coq{} :
 
 \fun{val Std.error : string -> 'a}
     {For simple error messages}
-\fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a}
+\fun{val Std.user_err : ?loc:Loc.t -> string -> std\_ppcmds -> 'a}
     {See Section~\ref{PrettyPrinter} : this can be used if the user
       want to display a term or build a complex error message}
 
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 17ff898b0..e14a2bd39 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -34,7 +34,7 @@ exception Timeout
 exception TacticFailure of exn
 
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.errorlabstrm "Some timeout function" (Pp.str"Timeout!")
+  | Timeout -> CErrors.user_err "Some timeout function" (Pp.str"Timeout!")
   | Exception e -> CErrors.print e
   | TacticFailure e -> CErrors.print e
   | _ -> Pervasives.raise CErrors.Unhandled
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 576569cf5..c47c44e22 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -365,7 +365,7 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
     let suffix = !nosuchgoals_hook n in
-    CErrors.errorlabstrm ""
+    CErrors.user_err ""
       (str "No such " ++ str (String.plural n "goal") ++ str "." ++
        pr_non_empty_arg (fun x -> x) suffix)
       | _ -> raise CErrors.Unhandled
@@ -451,7 +451,7 @@ let _ = CErrors.register_handler begin function
         str"Incorrect number of goals" ++ spc() ++
         str"(expected "++int i++str(String.plural i " tactic") ++ str")."
       in
-      CErrors.errorlabstrm "" errmsg
+      CErrors.user_err "" errmsg
   | _ -> raise CErrors.Unhandled
 end
 
@@ -849,7 +849,7 @@ let tclPROGRESS t =
 
 exception Timeout
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.errorlabstrm "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | Timeout -> CErrors.user_err "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
   | _ -> Pervasives.raise CErrors.Unhandled
 end
 
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 8dda4773e..db0f96715 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -300,7 +300,7 @@ let dirpath_of_string_list s =
   let id =
     try Nametab.full_name_module qid
     with Not_found ->
-      CErrors.errorlabstrm "Search.interface_search"
+      CErrors.user_err "Search.interface_search"
         (str "Module " ++ str path ++ str " not found.")
   in
   id
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f4907e92a..82039abd3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -366,7 +366,7 @@ let check_hidden_implicit_parameters id impls =
     | (Inductive indparams,_,_,_) -> Id.List.mem id indparams
     | _ -> false) impls
   then
-    errorlabstrm "" (strbrk "A parameter of an inductive type " ++
+    user_err "" (strbrk "A parameter of an inductive type " ++
     pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.")
 
 let push_name_env ?(global_level=false) ntnvars implargs env =
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 588637b76..19f76b972 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -86,7 +86,7 @@ let check_required_library d =
      (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
 *)
 (* or failing ...*)
-      errorlabstrm "Coqlib.check_required_library"
+      user_err "Coqlib.check_required_library"
         (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
 
 (************************************************************************)
diff --git a/interp/notation.ml b/interp/notation.ml
index 0c15e91b8..d50045546 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -95,7 +95,7 @@ let declare_scope scope =
     scope_map := String.Map.add scope empty_scope !scope_map
 
 let error_unknown_scope sc =
-  errorlabstrm "Notation"
+  user_err "Notation"
     (str "Scope " ++ str sc ++ str " is not declared.")
 
 let find_scope scope =
@@ -208,7 +208,7 @@ let remove_delimiters scope =
   let sc = find_scope scope in
   let newsc = { sc with delimiters = None } in
   match sc.delimiters with
-    | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
+    | None -> CErrors.user_err "" (str "No bound key for scope " ++ str scope ++ str ".")
     | Some key ->
        scope_map := String.Map.add scope newsc !scope_map;
        try
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7ab6ebb26..d565f01ba 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -377,7 +377,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
   let vars = Id.Map.filter filter nenv.ninterp_var_type in
   let check_recvar x =
     if Id.List.mem x found then
-      errorlabstrm "" (pr_id x ++
+      user_err "" (pr_id x ++
 	strbrk " should only be used in the recursive part of a pattern.") in
   let check (x, y) = check_recvar x; check_recvar y in
   let () = List.iter check foundrec in
@@ -396,7 +396,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) =
   in
   let check_pair s x y where =
     if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then
-      errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++
+      user_err "" (strbrk "in the right-hand side, " ++ pr_id x ++
 	str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++
 	str " position as part of a recursive pattern.") in
   let check_type x typ =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index f96d8acc1..1e0964dd2 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -30,7 +30,7 @@ let add_syntax_constant kn c onlyparse =
 
 let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
   if Nametab.exists_cci sp then
-    errorlabstrm "cache_syntax_constant"
+    user_err "cache_syntax_constant"
       (pr_id (basename sp) ++ str " already exists");
   add_syntax_constant kn pat onlyparse;
   Nametab.push_syndef (Nametab.Until i) sp kn
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 2d1ae68f4..9172fdbf0 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -907,7 +907,7 @@ let compile fail_on_error ?universes:(universes=0) env c =
       Feedback.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
     Some (init_code,!fun_code, Array.of_list fv)
   with TooLargeInductive tname ->
-    let fn = if fail_on_error then CErrors.errorlabstrm "compile" else
+    let fn = if fail_on_error then CErrors.user_err "compile" else
 	       (fun x -> Feedback.msg_warning x) in
       (Pp.(fn
 	   (str "Cannot compile code for virtual machine as it uses inductive " ++
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 09f7bd75c..e2ee913a3 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -816,7 +816,7 @@ let export ?except senv dir =
     try join_safe_environment ?except senv
     with e ->
       let e = CErrors.push e in
-      CErrors.errorlabstrm "export" (CErrors.iprint e)
+      CErrors.user_err "export" (CErrors.iprint e)
   in
   assert(senv.future_cst = []);
   let () = check_current_library dir senv in
@@ -852,7 +852,7 @@ let import lib cst vodigest senv =
   check_required senv.required lib.comp_deps;
   check_engagement senv.env lib.comp_enga;
   if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then
-    CErrors.errorlabstrm "Safe_typing.import"
+    CErrors.user_err "Safe_typing.import"
      (Pp.strbrk "Cannot load a library with the same name as the current one.");
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
diff --git a/kernel/term.ml b/kernel/term.ml
index 15f187e5c..340730558 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -465,7 +465,7 @@ let rec to_lambda n prod =
     match kind_of_term prod with
       | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd)
       | Cast (c,_,_) -> to_lambda n c
-      | _   -> errorlabstrm "to_lambda" (mt ())
+      | _   -> user_err "to_lambda" (mt ())
 
 let rec to_prod n lam =
   if Int.equal n 0 then
@@ -474,7 +474,7 @@ let rec to_prod n lam =
     match kind_of_term lam with
       | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd)
       | Cast (c,_,_) -> to_prod n c
-      | _   -> errorlabstrm "to_prod" (mt ())
+      | _   -> user_err "to_prod" (mt ())
 
 let it_mkProd_or_LetIn   = List.fold_left (fun c d -> mkProd_or_LetIn d c)
 let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 749b5dbaf..94a05ef67 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -276,7 +276,7 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
     if not (Id.Set.subset inferred_set declared_set) then
       let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
       let n = List.length l in
-      errorlabstrm "" (Pp.(str "The following section " ++
+      user_err "" (Pp.(str "The following section " ++
         str (String.plural n "variable") ++
         str " " ++ str (String.conjugate_verb_to_be n) ++
         str " used but not declared:" ++
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index c5f262373..830a9e3ce 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -34,17 +34,17 @@ let is_anomaly = function
 | _ -> false
 
 exception UserError of string * std_ppcmds (* User errors *)
-let error string = raise (UserError("_", str string))
-let errorlabstrm l pps = raise (UserError(l,pps))
-
-exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *)
-let alreadydeclared pps = raise (AlreadyDeclared(pps))
 
 let todo s = prerr_string ("TODO: "^s^"\n")
 
 let user_err    ?loc s strm = Loc.raise ?loc (UserError (s,strm))
+let error            string = user_err "_" (str string)
+
 let invalid_arg ?loc s   = Loc.raise ?loc (Invalid_argument s)
 
+exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *)
+let alreadydeclared pps = raise (AlreadyDeclared(pps))
+
 exception Timeout
 exception Drop
 exception Quit
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index 291c39b84..ad17be393 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -34,10 +34,13 @@ val is_anomaly : exn -> bool
     tricks with anomalies thanks to it. See rather [noncritical] below. *)
 
 exception UserError of string * std_ppcmds
-val error : string -> 'a
-val errorlabstrm : string -> std_ppcmds -> 'a
 
 val user_err     : ?loc:Loc.t -> string -> std_ppcmds -> 'a
+(** Main error raising primitive. [user_err ?loc c pp] signals an
+    error [pp] in component [c], with optional location [loc] *)
+
+val error : string -> 'a
+(** [error s] just calls [user_error "_" (str s)] *)
 
 exception AlreadyDeclared of std_ppcmds
 val alreadydeclared : std_ppcmds -> 'a
diff --git a/lib/system.ml b/lib/system.ml
index af9aa5c07..916c08795 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -132,7 +132,7 @@ let find_file_in_path ?(warn=true) paths filename =
       let root = Filename.dirname filename in
       root, filename
     else
-      CErrors.errorlabstrm "System.find_file_in_path"
+      CErrors.user_err "System.find_file_in_path"
 	(hov 0 (str "Can't find file" ++ spc () ++ str filename))
   else
     (* the name is considered to be the transcription as a relative
@@ -140,7 +140,7 @@ let find_file_in_path ?(warn=true) paths filename =
        to be locate respecting case *)
     try where_in_path ~warn paths filename
     with Not_found ->
-      CErrors.errorlabstrm "System.find_file_in_path"
+      CErrors.user_err "System.find_file_in_path"
 	(hov 0 (str "Can't find file" ++ spc () ++ str filename ++ spc () ++
 		str "on loadpath"))
 
@@ -163,7 +163,7 @@ let is_in_system_path filename =
 let open_trapping_failure name =
   try open_out_bin name
   with e when CErrors.noncritical e ->
-    CErrors.errorlabstrm "System.open" (str "Can't open " ++ str name)
+    CErrors.user_err "System.open" (str "Can't open " ++ str name)
 
 let warn_cannot_remove_file =
   CWarnings.create ~name:"cannot-remove-file" ~category:"filesystem"
@@ -175,7 +175,7 @@ let try_remove filename =
     warn_cannot_remove_file filename
 
 let error_corrupted file s =
-  CErrors.errorlabstrm "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
+  CErrors.user_err "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
 
 let input_binary_int f ch =
   try input_binary_int ch
@@ -252,7 +252,7 @@ let extern_state magic filename val_0 =
       let () = try_remove filename in
       iraise reraise
   with Sys_error s ->
-    CErrors.errorlabstrm "System.extern_state" (str "System error: " ++ str s)
+    CErrors.user_err "System.extern_state" (str "System error: " ++ str s)
 
 let intern_state magic filename =
   try
@@ -261,12 +261,12 @@ let intern_state magic filename =
     close_in channel;
     v
   with Sys_error s ->
-    CErrors.errorlabstrm "System.intern_state" (str "System error: " ++ str s)
+    CErrors.user_err "System.intern_state" (str "System error: " ++ str s)
 
 let with_magic_number_check f a =
   try f a
   with Bad_magic_number {filename=fname;actual=actual;expected=expected} ->
-    CErrors.errorlabstrm "with_magic_number_check"
+    CErrors.user_err "with_magic_number_check"
     (str"File " ++ str fname ++ strbrk" has bad magic number " ++
     int actual ++ str" (expected " ++ int expected ++ str")." ++
     spc () ++
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b2806a1ac..f388bc8b5 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -166,13 +166,13 @@ let consistency_checks exists dir dirinfo =
     let globref =
       try Nametab.locate_dir (qualid_of_dirpath dir)
       with Not_found ->
-        errorlabstrm "consistency_checks"
+        user_err "consistency_checks"
           (pr_dirpath dir ++ str " should already exist!")
     in
     assert (eq_global_dir_reference globref dirinfo)
   else
     if Nametab.exists_dir dir then
-      errorlabstrm "consistency_checks"
+      user_err "consistency_checks"
         (pr_dirpath dir ++ str " already exists")
 
 let compute_visibility exists i =
diff --git a/library/goptions.ml b/library/goptions.ml
index 0459417fb..b98cdac6a 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -36,7 +36,7 @@ type option_state = {
 let nickname table = String.concat " " table
 
 let error_undeclared_key key =
-  errorlabstrm "Goptions" (str (nickname key) ++ str ": no table or option of this type")
+  user_err "Goptions" (str (nickname key) ++ str ": no table or option of this type")
 
 (****************************************************************************)
 (* 1- Tables                                                                *)
diff --git a/library/impargs.ml b/library/impargs.ml
index 6da7e2110..f8990986c 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -339,14 +339,14 @@ let check_correct_manual_implicits autoimps l =
   List.iter (function
     | ExplByName id,(b,fi,forced) ->
 	if not forced then
-	  errorlabstrm ""
+	  user_err ""
             (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".")
     | ExplByPos (i,_id),_t ->
 	if i<1 || i>List.length autoimps then
-	  errorlabstrm ""
+	  user_err ""
             (str "Bad implicit argument number: " ++ int i ++ str ".")
 	else
-	  errorlabstrm ""
+	  user_err ""
 	    (str "Cannot set implicit argument number " ++ int i ++
 	      str ": it has no name.")) l
 
@@ -665,7 +665,7 @@ let check_inclusion l =
 
 let check_rigidity isrigid =
   if not isrigid then
-    errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
+    user_err "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.")
 
 let projection_implicits env p impls = 
   let pb = Environ.lookup_projection p env in
diff --git a/library/lib.ml b/library/lib.ml
index 8880a8b15..9d356bca8 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -75,7 +75,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 "Lib.classify_segment"
         (str "there are still opened " ++ str (module_kind ty) ++ str "s")
     | (_,FrozenState _) :: stk -> clean acc stk
   in
@@ -267,7 +267,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 "open_module" (pr_id id ++ str " already exists");
   add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
   path_prefix := prefix;
   prefix
@@ -277,7 +277,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 =
@@ -322,7 +322,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 "Lib.end_compilation_checks"
           (str "There are some open " ++ str (module_kind ty) ++ str "s.")
       | _ -> assert false
     with Not_found -> ()
@@ -374,7 +374,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 "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."
@@ -525,7 +525,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 "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*)
diff --git a/library/library.ml b/library/library.ml
index 0d65b3d0a..8d3916a97 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 "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 "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 "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 "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 "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) from in
   if not (Safe_typing.digest_match ~actual:digest ~required:d) then
-    errorlabstrm "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir);
+    user_err "" (str "Compiled library " ++ pr_dirpath caller ++ str ".vo makes inconsistent assumptions over library " ++ pr_dirpath dir);
   libs
 
 let rec_intern_library libs (dir, f) =
@@ -609,7 +609,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.")
 
@@ -622,7 +622,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
@@ -658,10 +658,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 "restart" (str"not a .vio file");
+  if s2 = None then user_err "restart" (str"not a .vio file");
+  if s3 = None then user_err "restart" (str"not a .vio file");
+  if pi3 (Option.get s2) then user_err "restart" (str"not a .vio file");
   longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
@@ -677,7 +677,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.")
@@ -724,7 +724,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 "library"
       Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
     opaque_table;
   let sd = {
diff --git a/library/universes.ml b/library/universes.ml
index db95607f1..04b39937e 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -337,7 +337,7 @@ let existing_instance ctx inst =
     and a2 = Instance.to_array (UContext.instance ctx) in
     let len1 = Array.length a1 and len2 = Array.length a2 in 
       if not (len1 == len2) then
-	CErrors.errorlabstrm "Universes"
+	CErrors.user_err "Universes"
 	  (str "Polymorphic constant expected " ++ int len2 ++ 
 	     str" levels but was given " ++ int len1)
       else ()
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 47c78ae5c..e0583370a 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1508,7 +1508,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
 	Evar.Set.fold 
 	  (fun ev acc -> 
 	   if not (Evd.is_defined acc ev) then 
-	     errorlabstrm "rewrite"
+	     user_err "rewrite"
 			  (str "Unsolved constraint remaining: " ++ spc () ++
 			   Evd.pr_evar_info (Evd.find acc ev))
 	   else Evd.remove acc ev) 
@@ -1647,7 +1647,7 @@ let cl_rewrite_clause_strat progress strat clause =
    (fun gl -> 
     try Proofview.V82.of_tactic (cl_rewrite_clause_newtac ~progress strat clause) gl
     with RewriteFailure e ->
-	 errorlabstrm "" (str"setoid rewrite failed: " ++ e)
+	 user_err "" (str"setoid rewrite failed: " ++ e)
        | Refiner.FailError (n, pp) -> 
 	  tclFAIL n (str"setoid rewrite failed: " ++ Lazy.force pp) gl))
 
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index c709ab114..5808feeba 100644
--- a/ltac/tacenv.ml
+++ b/ltac/tacenv.ml
@@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } =
     let () = if Array.length tacs <= i then raise Not_found in
     tacs.(i)
   with Not_found ->
-    CErrors.errorlabstrm ""
+    CErrors.user_err ""
       (str "The tactic " ++ pr_tacname s ++ str " is not installed.")
 
 (***************************************************************************)
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index dc216da11..a1d34b53f 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -748,7 +748,7 @@ let print_ltac id =
     ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
  with
   Not_found ->
-   errorlabstrm "print_ltac"
+   user_err "print_ltac"
     (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
 
 (** Registering *)
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 76c46ea7c..b1f554eaa 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -168,7 +168,7 @@ module Value = struct
     let pr_v = Pptactic.pr_value Pptactic.ltop v in
     let Val.Dyn (tag, _) = v in
     let tag = Val.pr tag in
-    errorlabstrm "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
+    user_err "" (str "Type error: value " ++ pr_v ++ str " is a " ++ tag
       ++ str " while type " ++ Val.pr wit ++ str " was expected.")
 
   let unbox wit v ans = match ans with
@@ -1870,7 +1870,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
               let (sigma, c) = interp_constr ist env sigma c in
               Sigma.Unsafe.of_pair (c, sigma)
             with e when to_catch e (* Hack *) ->
-              errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
+              user_err "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
         end } in
         Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)
       end }
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 65d49cb45..7d3cb7e49 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -71,7 +71,7 @@ let error_level_assoc p current expected =
     | Extend.LeftA -> str "left"
     | Extend.RightA -> str "right"
     | Extend.NonA -> str "non" in
-  errorlabstrm ""
+  user_err ""
     (str "Level " ++ int p ++ str " is already declared " ++
      pr_assoc current ++ str " associative while it is now expected to be " ++
      pr_assoc expected ++ str " associative.")
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index fd46d8069..6ed678176 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -456,7 +456,7 @@ let cc_tactic depth additionnal_terms =
   end }
 
 let cc_fail gls =
-  errorlabstrm  "Congruence" (Pp.str "congruence failed.")
+  user_err  "Congruence" (Pp.str "congruence failed.")
 
 let congruence_tac depth l =
   Tacticals.New.tclORELSE
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 49843d828..9ed5c61e2 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -328,7 +328,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
   let _ =
     let expected = mib.Declarations.mind_nparams - num_params in
       if not (Int.equal (List.length params) expected) then
-	errorlabstrm "suppose it is" 
+	user_err "suppose it is" 
 	  (str "Wrong number of extra arguments: " ++ 
 	     (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
 	     str "expected.") in
@@ -348,7 +348,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
       Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp)
     | Thesis (For rec_occ) ->
 	if not (Id.List.mem rec_occ pat_vars) then
-	  errorlabstrm "suppose it is"
+	  user_err "suppose it is"
 	    (str "Variable " ++ Nameops.pr_id rec_occ ++
 	       str " does not occur in pattern.");
 	Glob_term.GSort(Loc.ghost,GProp)
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 97c9d5f4a..9510ba384 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -43,7 +43,7 @@ let clear ids { it = goal; sigma } =
   let (hyps, concl) =
     try Evarutil.clear_hyps_in_evi env evdref sign cl ids
     with Evarutil.ClearDependencyError (id, _) ->
-      errorlabstrm "" (str "Cannot clear " ++ pr_id id)
+      user_err "" (str "Cannot clear " ++ pr_id id)
   in
   let sigma = !evdref in
   let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
@@ -1082,12 +1082,12 @@ let thesis_for obj typ per_info env=
   let cind,all_args=decompose_app typ in
   let ind,u = destInd cind in
   let _ = if not (eq_ind ind per_info.per_ind) then
-    errorlabstrm "thesis_for"
+    user_err "thesis_for"
       ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
 	 str"cannot give an induction hypothesis (wrong inductive type).") in
   let params,args = List.chop per_info.per_nparams all_args in
   let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
-    errorlabstrm "thesis_for"
+    user_err "thesis_for"
       ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
 	 str "cannot give an induction hypothesis (wrong parameters).") in
   let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ff66d915f..3c26c4710 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -293,7 +293,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
 (*S Warning and Error messages. *)
 
-let err s = errorlabstrm "Extraction" s
+let err s = user_err "Extraction" s
 
 let warn_extraction_axiom_to_realize =
   CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction"
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 5e72b8672..f4daa0323 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -609,7 +609,7 @@ let build_scheme fas =
 	      try
 		Smartlocate.global_with_alias f
 	      with Not_found ->
-                errorlabstrm "FunInd.build_scheme"
+                user_err "FunInd.build_scheme"
                   (str "Cannot find " ++ Libnames.pr_reference f)
 	    in
 	    let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
@@ -643,7 +643,7 @@ let build_case_scheme fa =
     let (_,f,_) = fa in
     try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
     with Not_found ->
-      errorlabstrm "FunInd.build_case_scheme"
+      user_err "FunInd.build_case_scheme"
         (str "Cannot find " ++ Libnames.pr_reference f) in
   let first_fun,u = destConst  funs in
   let funs_mp,funs_dp,_ = Names.repr_con first_fun in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 5548833d6..9902b0128 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -630,7 +630,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let (ind,_) =
 	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	  with Not_found ->
-	    errorlabstrm "" (str "Cannot find the inductive associated to " ++
+	    user_err "" (str "Cannot find the inductive associated to " ++
 			       Printer.pr_glob_constr b ++ str " in " ++
 			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	in
@@ -662,7 +662,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	  let (ind,_) =
 	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
 	    with Not_found ->
-	      errorlabstrm "" (str "Cannot find the inductive associated to " ++
+	      user_err "" (str "Cannot find the inductive associated to " ++
 				 Printer.pr_glob_constr b ++ str " in " ++
 				 Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	  in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4f183b3a1..943ebc9fc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -42,7 +42,7 @@ let functional_induction with_clean c princl pat =
 		let finfo = (* we first try to find out a graph on f *)
 		  try find_Function_infos c'
 		  with Not_found ->
-		    errorlabstrm "" (str "Cannot find induction information on "++
+		    user_err "" (str "Cannot find induction information on "++
 				       Printer.pr_lconstr (mkConst c') )
 		in
 		match Tacticals.elimination_sort_of_goal g with
@@ -70,7 +70,7 @@ let functional_induction with_clean c princl pat =
 		    (b,a)
 		    (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
 		  with Not_found -> (* This one is neither defined ! *)
-		    errorlabstrm "" (str "Cannot find induction principle for "
+		    user_err "" (str "Cannot find induction principle for "
 				     ++Printer.pr_lconstr (mkConst c') )
 	      in
 	      (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g')
@@ -321,7 +321,7 @@ let error_error names e =
   in
   match e with
     | Building_graph e ->
-	errorlabstrm ""
+	user_err ""
 	  (str "Cannot define graph(s) for " ++
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	     e_explain e)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f56e92414..a1c94f8cb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -110,7 +110,7 @@ let const_of_id id =
   in
   try Constrintern.locate_reference princ_ref
   with Not_found ->
-    CErrors.errorlabstrm "IndFun.const_of_id"
+    CErrors.user_err "IndFun.const_of_id"
       (str "cannot find " ++ Nameops.pr_id id)
 
 let def_of_const t =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 26fc88a60..ee1232013 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1043,19 +1043,19 @@ let invfun qhyp f g =
 			 functional_inversion kn hid  f2 f_correct g
 		       with
 			 | Failure "" ->
-			     errorlabstrm "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
+			     user_err "" (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
 			 | Option.IsNone  ->
 			     if do_observe ()
 			     then
 			       error "Cannot use equivalence with graph for any side of the equality"
-			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+			     else user_err "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
 			 | Not_found ->
 			     if do_observe ()
 			     then
 			       error "No graph found for any side of equality"
-			     else errorlabstrm "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+			     else user_err "" (str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
 		   end
-	       | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
+	       | _ -> user_err "" (Ppconstr.pr_id hid ++ str " must be an equality ")
 	  end)
 	  qhyp
           end
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index de4210af5..0b93a909a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -901,7 +901,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
       locate_constant f_ref in
     try find_Function_infos (kn_of_id id)
     with Not_found ->
-      errorlabstrm "indfun" (Nameops.pr_id id ++ str " has no functional scheme")
+      user_err "indfun" (Nameops.pr_id id ++ str " has no functional scheme")
 
 (** [merge id1 id2 args1 args2 id] builds and declares a new inductive
     type called [id], representing the merged graphs of both graphs
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 62f307115..7745e8498 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -307,7 +307,7 @@ let check_not_nested forbidden e =
       | Rel _ -> ()
       | Var x ->
         if Id.List.mem x forbidden
-        then errorlabstrm "Recdef.check_not_nested"
+        then user_err "Recdef.check_not_nested"
                (str "check_not_nested: failure " ++ pr_id x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
@@ -327,7 +327,7 @@ let check_not_nested forbidden e =
   try 
     check_not_nested e 
   with UserError(_,p) -> 
-    errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
+    user_err "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
 
 (* ['a info] contains the local information for traveling *)
 type 'a infos = 
@@ -442,7 +442,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info
 	with e when CErrors.noncritical e ->
-	  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+	  user_err "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Lambda(n,t,b) -> 
       begin
@@ -450,7 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	  check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info
 	with e when CErrors.noncritical e ->
-	  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+	  user_err "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
       end
     | Case(ci,t,a,l) -> 
       begin
@@ -478,7 +478,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
 	      jinfo.apP (f,args) expr_info continuation_tac in 
 	    travel_args jinfo
 	      expr_info.is_main_branch new_continuation_tac new_infos
-	  | Case _ ->  errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
+	  | Case _ ->  user_err "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)")
 	  | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_lconstr expr_info.info)
       end
     | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t}
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 4ed907951..9cfcb0fb7 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -263,7 +263,7 @@ let rtauto_tac gls=
   let _=
     if Retyping.get_sort_family_of
       (pf_env gls) (Tacmach.project gls) gl != InProp
-    then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in
+    then user_err "rtauto" (Pp.str "goal should be in Prop") in
   let glf=make_form gamma gls gl in
   let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in
   let formula=
@@ -282,7 +282,7 @@ let rtauto_tac gls=
   let prf =
     try project (search_fun (init_state [] formula))
     with Not_found ->
-      errorlabstrm "rtauto" (Pp.str "rtauto couldn't find any proof") in
+      user_err "rtauto" (Pp.str "rtauto couldn't find any proof") in
   let search_end_time = System.get_time () in
   let _ = if !verbose then
     begin
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 90f5f8e63..7450aa23e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -79,7 +79,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps
 let lookup_map map =
   try String.Map.find map !protect_maps
   with Not_found ->
-    errorlabstrm"lookup_map"(str"map "++qs map++str"not found")
+    user_err"lookup_map"(str"map "++qs map++str"not found")
 
 let protect_red map env sigma c =
   kl (create_clos_infos all env)
@@ -348,13 +348,13 @@ let find_ring_structure env sigma l =
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
           if not (Reductionops.is_conv env sigma ty ty') then
-            errorlabstrm "ring"
+            user_err "ring"
               (str"arguments of ring_simplify do not have all the same type")
         in
         List.iter check cl';
         (try ring_for_carrier ty
         with Not_found ->
-          errorlabstrm "ring"
+          user_err "ring"
             (str"cannot find a declared ring structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
     | [] -> assert false
@@ -828,13 +828,13 @@ let find_field_structure env sigma l =
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
           if not (Reductionops.is_conv env sigma ty ty') then
-            errorlabstrm "field"
+            user_err "field"
               (str"arguments of field_simplify do not have all the same type")
         in
         List.iter check cl';
         (try field_for_carrier ty
         with Not_found ->
-          errorlabstrm "field"
+          user_err "field"
             (str"cannot find a declared field structure over"++
              spc()++str"\""++pr_constr ty++str"\""))
     | [] -> assert false
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 536c6ff4b..199c26363 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -61,7 +61,7 @@ DECLARE PLUGIN "ssrmatching_plugin"
 
 type loc = Loc.t
 let dummy_loc = Loc.ghost
-let errorstrm = CErrors.errorlabstrm "ssrmatching"
+let errorstrm = CErrors.user_err "ssrmatching"
 let loc_error loc msg = CErrors.user_err ~loc msg (str msg)
 let ppnl = Feedback.msg_info
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 85c518019..18ad2ed3d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -503,7 +503,7 @@ let set_used_pattern eqn = eqn.used := true
 
 let extract_rhs pb =
   match pb.mat with
-    | [] -> errorlabstrm "build_leaf" (msg_may_need_inversion())
+    | [] -> user_err "build_leaf" (msg_may_need_inversion())
     | eqn::_ ->
 	set_used_pattern eqn;
         eqn.rhs
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 4f265e76c..92a0ca988 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -538,7 +538,7 @@ let inheritance_graph () =
 let coercion_of_reference r =
   let ref = Nametab.global r in
   if not (coercion_exists ref) then
-    errorlabstrm "try_add_coercion"
+    user_err "try_add_coercion"
       (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion.");
   ref
 
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 4caa1e992..c7909a3c7 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -35,7 +35,7 @@ let explain_occurrence_error = function
   | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id
 
 let error_occurrences_error e =
-  errorlabstrm "" (explain_occurrence_error e)
+  user_err "" (explain_occurrence_error e)
 
 let error_invalid_occurrence occ =
   error_occurrences_error (InvalidOccurrence occ)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 39aeb41f7..0061d8ae9 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -55,7 +55,7 @@ let is_private mib =
 
 let check_privacy_block mib =
   if is_private mib then
-    errorlabstrm ""(str"case analysis on a private inductive type")
+    user_err ""(str"case analysis on a private inductive type")
       
 (**********************************************************************)
 (* Building case analysis schemes *)
@@ -594,7 +594,7 @@ let lookup_eliminator ind_sp s =
   (* using short name (e.g. for "eq_rec") *)
   try Nametab.locate (qualid_of_ident id)
   with Not_found ->
-    errorlabstrm "default_elim"
+    user_err "default_elim"
       (strbrk "Cannot find the elimination combinator " ++
        pr_id id ++ strbrk ", the elimination of the inductive definition " ++
        pr_global_env Id.Set.empty (IndRef ind_sp) ++
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 214e19fec..cb69ab36f 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -355,7 +355,7 @@ let make_case_or_project env indf ci pred c branches =
        let mib, _ = Inductive.lookup_mind_specif env ind in
        if (* dependent *) not (noccurn 1 t) &&
           not (has_dependent_elim mib) then
-       errorlabstrm "make_case_or_project"
+       user_err "make_case_or_project"
 		    Pp.(str"Dependent case analysis not allowed" ++
 		     str" on inductive type " ++ Names.MutInd.print (fst ind))
      in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 99c3772db..aa795106a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -204,7 +204,7 @@ let error_instantiate_pattern id l =
   | [_] -> "is" 
   | _ -> "are"
   in
-  errorlabstrm "" (str "Cannot substitute the term bound to " ++ pr_id id
+  user_err "" (str "Cannot substitute the term bound to " ++ pr_id id
     ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
     ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8b0bdb009..cdb39207e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -390,7 +390,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
       try Name (Id.Map.find id ltac_idents)
       with Not_found ->
         if Id.Map.mem id ltac_genargs then
-          errorlabstrm "" (str"Ltac variable"++spc()++ pr_id id ++
+          user_err "" (str"Ltac variable"++spc()++ pr_id id ++
                            spc()++str"is not bound to an identifier."++spc()++
                            str"It cannot be used in a binder.")
         else n
@@ -411,14 +411,14 @@ let invert_ltac_bound_name lvar env id0 id =
   let id' = Id.Map.find id lvar.ltac_idents in
   try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
   with Not_found ->
-    errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+    user_err "" (str "Ltac variable " ++ pr_id id0 ++
 		       str " depends on pattern variable name " ++ pr_id id ++
 		       str " which is not bound in current context.")
 
 let protected_get_type_of env sigma c =
   try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
   with Retyping.RetypeError _ ->
-    errorlabstrm ""
+    user_err ""
       (str "Cannot reinterpret " ++ quote (print_constr c) ++
        str " in the current environment.")
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 284af0cb1..945ef5daa 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -291,7 +291,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
 (*s High-level declaration of a canonical structure *)
 
 let error_not_structure ref =
-  errorlabstrm "object_declare"
+  user_err "object_declare"
     (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.")
 
 let check_and_decompose_canonical_structure ref =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 820a81b5d..67819dc98 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -38,7 +38,7 @@ exception Elimconst
 exception Redelimination
 
 let error_not_evaluable r =
-  errorlabstrm "error_not_evaluable"
+  user_err "error_not_evaluable"
     (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++
      spc () ++ str "to an evaluable reference.")
 
@@ -993,7 +993,7 @@ let e_contextually byhead (occs,c) f = { e_redfun = begin fun env sigma t ->
       incr pos;
       if ok then begin
         if Option.has_some nested then
-          errorlabstrm "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
+          user_err "" (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
         (* Skip inner occurrences for stable counting of occurrences *)
         if locs != [] then
           ignore (traverse_below (Some (!pos-1)) envc t);
@@ -1159,13 +1159,13 @@ let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c ->
 let check_privacy env ind =
   let spec = Inductive.lookup_mind_specif env (fst ind) in
   if Inductive.is_private spec then
-    errorlabstrm "" (str "case analysis on a private type.")
+    user_err "" (str "case analysis on a private type.")
   else ind
 
 let check_not_primitive_record env ind =
   let spec = Inductive.lookup_mind_specif env (fst ind) in
     if Inductive.is_primitive_record spec then
-      errorlabstrm "" (str "case analysis on a primitive record type: " ++
+      user_err "" (str "case analysis on a primitive record type: " ++
 		       str "use projections or let instead.")
     else ind
 
@@ -1182,14 +1182,14 @@ let reduce_to_ind_gen allow_product env sigma t =
 	  if allow_product then
 	    elimrec (push_rel (LocalAssum (n,ty)) env) t' ((LocalAssum (n,ty))::l)
 	  else
-	    errorlabstrm "" (str"Not an inductive definition.")
+	    user_err "" (str"Not an inductive definition.")
       | _ ->
 	  (* Last chance: we allow to bypass the Opaque flag (as it
 	     was partially the case between V5.10 and V8.1 *)
 	  let t' = whd_all env sigma t in
 	  match kind_of_term (fst (decompose_app t')) with
 	    | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l)
-	    | _ -> errorlabstrm "" (str"Not an inductive product.")
+	    | _ -> user_err "" (str"Not an inductive product.")
   in
   elimrec env t []
 
@@ -1239,7 +1239,7 @@ let one_step_reduce env sigma c =
   applist (redrec (c,[]))
 
 let error_cannot_recognize ref =
-  errorlabstrm ""
+  user_err ""
     (str "Cannot recognize a statement based on " ++
      Nametab.pr_global_env Id.Set.empty ref ++ str".")
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0c1ce0d2f..5e3c3c259 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1586,7 +1586,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     let ids = ids_of_named_context (named_context env) in
     if name == Anonymous then next_ident_away_in_goal x ids else
     if mem_named_context x (named_context env) then
-      errorlabstrm "Unification.make_abstraction_core"
+      user_err "Unification.make_abstraction_core"
         (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
     else
       x
@@ -1600,7 +1600,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         if indirectly_dependent c d depdecls then
           (* Told explicitly not to abstract over [d], but it is dependent *)
           let id' = indirect_dependency d depdecls in
-          errorlabstrm "" (str "Cannot abstract over " ++ Nameops.pr_id id'
+          user_err "" (str "Cannot abstract over " ++ Nameops.pr_id id'
             ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp
             ++ str ".")
         else
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index a7742d866..e2fefa5c8 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -736,7 +736,7 @@ let print_any_name = function
     let open Context.Named.Declaration in
     str |> Global.lookup_named |> set_id str |> print_named_decl
   with Not_found ->
-    errorlabstrm
+    user_err
       "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
 let print_name = function
@@ -831,7 +831,7 @@ let index_of_class cl =
   try
     fst (class_info cl)
   with Not_found ->
-    errorlabstrm "index_of_class"
+    user_err "index_of_class"
       (pr_class cl ++ spc() ++ str "not a defined class.")
 
 let print_path_between cls clt =
@@ -841,7 +841,7 @@ let print_path_between cls clt =
     try
       lookup_path_between_class (i,j)
     with Not_found ->
-      errorlabstrm "index_cl_of_id"
+      user_err "index_cl_of_id"
         (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt
 	 ++ str ".")
   in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0a90e0dbd..0ee13bb63 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -155,7 +155,7 @@ let error_incompatible_inst clenv mv  =
   let na = meta_name clenv.evd mv in
   match na with
       Name id ->
-        errorlabstrm "clenv_assign"
+        user_err "clenv_assign"
           (str "An incompatible instantiation has already been found for " ++
            pr_id id)
     | _ ->
@@ -417,11 +417,11 @@ let qhyp_eq h1 h2 = match h1, h2 with
 let check_bindings bl =
   match List.duplicates qhyp_eq (List.map pi2 bl) with
     | NamedHyp s :: _ ->
-	errorlabstrm ""
+	user_err ""
 	  (str "The variable " ++ pr_id s ++
 	   str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
-	errorlabstrm ""
+	user_err ""
 	  (str "The position " ++ int n ++
 	   str " occurs more than once in binding list.")
     | [] -> ()
@@ -435,7 +435,7 @@ let explain_no_such_bound_variable evd id =
     if na != Anonymous then out_name na :: l else l
   in
   let mvl = List.fold_left fold [] (Evd.meta_list evd) in
-  errorlabstrm "Evd.meta_with_name"
+  user_err "Evd.meta_with_name"
     (str"No such bound variable " ++ pr_id id ++
      (if mvl == [] then str " (no bound variables at all in the expression)."
       else
@@ -460,7 +460,7 @@ let meta_with_name evd id =
     | ([n],_|_,[n]) ->
         n
     | _  ->
-        errorlabstrm "Evd.meta_with_name"
+        user_err "Evd.meta_with_name"
           (str "Binder name \"" ++ pr_id id ++
            strbrk "\" occurs more than once in clause.")
 
@@ -469,12 +469,12 @@ let meta_of_binder clause loc mvs = function
   | AnonHyp n ->
       try List.nth mvs (n-1)
       with (Failure _|Invalid_argument _) ->
-        errorlabstrm "" (str "No such binder.")
+        user_err "" (str "No such binder.")
 
 let error_already_defined b =
   match b with
     | NamedHyp id ->
-        errorlabstrm ""
+        user_err ""
           (str "Binder name \"" ++ pr_id id ++
            str"\" already defined with incompatible value.")
     | AnonHyp n ->
@@ -527,7 +527,7 @@ let clenv_constrain_last_binding c clenv =
   clenv_assign_binding clenv k c
 
 let error_not_right_number_missing_arguments n =
-  errorlabstrm ""
+  user_err ""
     (strbrk "Not the right number of missing arguments (expected " ++
       int n ++ str ").")
 
@@ -641,7 +641,7 @@ let explain_no_such_bound_variable holes id =
   | [id] -> str "(possible name is: " ++ pr_id id ++ str ")."
   | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")."
   in
-  errorlabstrm "" (str "No such bound variable " ++ pr_id id ++ expl)
+  user_err "" (str "No such bound variable " ++ pr_id id ++ expl)
 
 let evar_with_name holes id =
   let map h = match h.hole_name with
@@ -653,7 +653,7 @@ let evar_with_name holes id =
   | [] -> explain_no_such_bound_variable holes id
   | [h] -> h.hole_evar
   | _ ->
-    errorlabstrm ""
+    user_err ""
       (str "Binder name \"" ++ pr_id id ++
         str "\" occurs more than once in clause.")
 
@@ -664,7 +664,7 @@ let evar_of_binder holes = function
     let h = List.nth holes (pred n) in
     h.hole_evar
   with e when CErrors.noncritical e ->
-    errorlabstrm "" (str "No such binder.")
+    user_err "" (str "No such binder.")
 
 let define_with_type sigma env ev c =
   let t = Retyping.get_type_of env sigma ev in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index aa0b9bac6..9f34f5cf6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -151,7 +151,7 @@ let reorder_context env sign ord =
       | top::ord' when mem_q top moved_hyps ->
           let ((d,h),mh) = find_q top moved_hyps in
           if occur_vars_in_decl env h d then
-            errorlabstrm "reorder_context"
+            user_err "reorder_context"
               (str "Cannot move declaration " ++ pr_id top ++ spc() ++
               str "before " ++
               pr_sequence pr_id
@@ -182,7 +182,7 @@ let check_decl_position env sign d =
   let needed = global_vars_set_of_decl env d in
   let deps = dependency_closure env (named_context_of_val sign) needed in
   if Id.List.mem x deps then
-    errorlabstrm "Logic.check_decl_position"
+    user_err "Logic.check_decl_position"
       (str "Cannot create self-referring hypothesis " ++ pr_id x);
   x::deps
 
@@ -252,7 +252,7 @@ let move_hyp toleft (left,declfrom,right) hto =
 	    if not (move_location_eq hto (MoveAfter hyp)) then
 	      (first, d::middle)
             else
-	      errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++
+	      user_err "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++
 	        Miscprint.pr_move_location pr_id hto ++
 	        str (if toleft then ": it occurs in " else ": it depends on ")
 	        ++ pr_id hyp ++ str ".")
@@ -287,7 +287,7 @@ let move_hyp toleft (left,declfrom,right) hto =
 variables only in Application and Case *)
 
 let error_unsupported_deep_meta c =
-  errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++
+  user_err "" (strbrk "Application of lemmas whose beta-iota normal " ++
     strbrk "form contains metavariables deep inside the term is not " ++
     strbrk "supported; try \"refine\" instead.")
 
@@ -498,10 +498,10 @@ let convert_hyp check sign sigma d =
         let _,c,ct = to_tuple d' in
         let env = Global.env_of_context sign in
         if check && not (is_conv env sigma bt ct) then
-	  errorlabstrm "Logic.convert_hyp"
+	  user_err "Logic.convert_hyp"
             (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
-	  errorlabstrm "Logic.convert_hyp"
+	  user_err "Logic.convert_hyp"
             (str "Incorrect change of the body of "++ pr_id id ++ str ".");
        if check then reorder := check_decl_position env sign d;
        d) in
@@ -534,7 +534,7 @@ let prim_refiner r sigma goal =
 	      t,cl,sigma
 	  else
             (if !check && mem_named_context id (named_context_of_val sign) then
-	      errorlabstrm "Logic.prim_refiner"
+	      user_err "Logic.prim_refiner"
                 (str "Variable " ++ pr_id id ++ str " is already declared.");
 	     push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index e4bae2012..b86582def 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -131,7 +131,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     | CList.IndexOutOfRange ->
         match gi with
 	| Vernacexpr.SelectNth i -> let msg = str "No such goal: " ++ int i ++ str "." in
-	                            CErrors.errorlabstrm "" msg
+	                            CErrors.user_err "" msg
         | _ -> assert false
 
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 5fe29653d..2e5330b4b 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -68,9 +68,9 @@ let _ = CErrors.register_handler begin function
   | CannotUnfocusThisWay ->
     CErrors.error "This proof is focused, but cannot be unfocused this way"
   | NoSuchGoals (i,j) when Int.equal i j ->
-      CErrors.errorlabstrm "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+      CErrors.user_err "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
-      CErrors.errorlabstrm "Focus" Pp.(
+      CErrors.user_err "Focus" Pp.(
         str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
       )
   | FullyUnfocused -> CErrors.error "The proof is not focused"
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 7b43b64ef..107a3a7e5 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -519,7 +519,7 @@ module Bullet = struct
 	(function
 	| FailedBullet (b,sugg) ->
 	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
-	  CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
+	  CErrors.user_err "Focus" (prefix ++ suggest_on_error sugg)
 	| _ -> raise CErrors.Unhandled)
 
 
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 8a9ce4f94..cafd46849 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -73,7 +73,7 @@ let set_strategy_one ref l  =
         let cb = Global.lookup_constant sp in
 	(match cb.const_body with
 	  | OpaqueDef _ ->
-            errorlabstrm "set_transparent_const"
+            user_err "set_transparent_const"
               (str "Cannot make" ++ spc () ++
 		 Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++
 		 spc () ++ str "transparent because it was declared opaque.");
@@ -175,19 +175,19 @@ let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
 
 let declare_reduction s f =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then errorlabstrm "Redexpr.declare_reduction"
+  then user_err "Redexpr.declare_reduction"
     (str "There is already a reduction expression of name " ++ str s)
   else reduction_tab := String.Map.add s f !reduction_tab
 
 let check_custom = function
   | ExtraRedExpr s ->
       if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
-      then errorlabstrm "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
+      then user_err "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
   |_ -> ()
 
 let decl_red_expr s e =
   if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
-  then errorlabstrm "Redexpr.decl_red_expr"
+  then user_err "Redexpr.decl_red_expr"
     (str "There is already a reduction expression of name " ++ str s)
   else begin
     check_custom e;
@@ -247,7 +247,7 @@ let reduction_of_red_expr env =
       with Not_found ->
 	(try reduction_of_red_expr (String.Map.find s !red_expr_tab)
 	 with Not_found ->
-	   errorlabstrm "Redexpr.reduction_of_red_expr"
+	   user_err "Redexpr.reduction_of_red_expr"
              (str "unknown user-defined reduction \"" ++ str s ++ str "\"")))
   | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast)
   | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast)
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ebd30820b..65a889882 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -60,7 +60,7 @@ let tclIDTAC_MESSAGE s gls =
   Feedback.msg_info (hov 0 s); tclIDTAC gls
 
 (* General failure tactic *)
-let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s)
+let tclFAIL_s s gls = user_err "Refiner.tclFAIL_s" (str s)
 
 (* A special exception for levels for the Fail tactic *)
 exception FailError of int * std_ppcmds Lazy.t
@@ -82,7 +82,7 @@ let thens3parts_tac tacfi tac tacli (sigr,gs) =
   let nf = Array.length tacfi in
   let nl = Array.length tacli in
   let ng = List.length gs in
-  if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
+  if ng<nf+nl then user_err "Refiner.thensn_tac" (str "Not enough subgoals.");
   let gll =
       (List.map_i (fun i ->
         apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
@@ -164,14 +164,14 @@ the goal unchanged *)
 let tclWEAK_PROGRESS tac ptree =
   let rslt = tac ptree in
   if Goal.V82.weak_progress rslt ptree then rslt
-  else errorlabstrm "Refiner.WEAK_PROGRESS" (str"Failed to progress.")
+  else user_err "Refiner.WEAK_PROGRESS" (str"Failed to progress.")
 
 (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
 the goal unchanged *)
 let tclPROGRESS tac ptree =
   let rslt = tac ptree in
   if Goal.V82.progress rslt ptree then rslt
-  else errorlabstrm "Refiner.PROGRESS" (str"Failed to progress.")
+  else user_err "Refiner.PROGRESS" (str"Failed to progress.")
 
 (* Same as tclWEAK_PROGRESS but fails also if tactics generates several goals,
    one of them being identical to the original goal *)
@@ -182,7 +182,7 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
   let rslt = tac goal in
   let {it=gls;sigma=sigma} = rslt in
   if List.exists (same_goal goal sigma) gls
-  then errorlabstrm "Refiner.tclNOTSAMEGOAL"
+  then user_err "Refiner.tclNOTSAMEGOAL"
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
@@ -316,7 +316,7 @@ let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl)
 
 let tclDO n t =
   let rec dorec k =
-    if k < 0 then errorlabstrm "Refiner.tclDO"
+    if k < 0 then user_err "Refiner.tclDO"
       (str"Wrong argument : Do needs a positive integer.");
     if Int.equal k 0 then tclIDTAC
     else if Int.equal k 1 then t else (tclTHEN t (dorec (k-1)))
diff --git a/stm/stm.ml b/stm/stm.ml
index 9f86597dc..ff4688480 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 "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 "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 "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 "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 "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 "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 "stm" (str"Cannot dump a vio with open proofs");
   Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
     (Global.opaque_tables ())
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 3257d406a..b898ceb04 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -65,7 +65,7 @@ let raw_find_base bas = String.Map.find bas !rewtab
 let find_base bas =
   try raw_find_base bas
   with Not_found ->
-    errorlabstrm "AutoRewrite"
+    user_err "AutoRewrite"
       (str "Rewriting base " ++ str bas ++ str " does not exist.")
 
 let find_rewrites bas =
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2eca1e597..dcf3dea10 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -98,7 +98,7 @@ let prolog_tac l n =
   let l = List.map map l in
   try (prolog l n gl)
   with UserError ("Refiner.tclFIRST",_) ->
-    errorlabstrm "Prolog.prolog" (str "Prolog failed.")
+    user_err "Prolog.prolog" (str "Prolog failed.")
   end
 
 open Auto
@@ -431,7 +431,7 @@ let cons a l = a :: l
 let autounfolds db occs cls gl =
   let unfolds = List.concat (List.map (fun dbname -> 
     let db = try searchtable_map dbname 
-      with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+      with Not_found -> user_err "autounfold" (str "Unknown database " ++ str dbname)
     in
     let (ids, csts) = Hint_db.unfolds db in
     let hyps = pf_ids_of_hyps gl in
@@ -498,7 +498,7 @@ let autounfold_one db cl =
   let st =
     List.fold_left (fun (i,c) dbname -> 
       let db = try searchtable_map dbname 
-	with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
+	with Not_found -> user_err "autounfold" (str "Unknown database " ++ str dbname)
       in
       let (ids, csts) = Hint_db.unfolds db in
 	(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2c97cf442..4391a96b1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -359,7 +359,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	      let _ = Global.lookup_constant c1' in
 		c1'
 	    with Not_found -> 
-	      errorlabstrm "Equality.find_elim"
+	      user_err "Equality.find_elim"
                 (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
 	  end
 	| _ -> destConstRef pr1
@@ -888,7 +888,7 @@ let build_selector env sigma dirn c ind special default =
           on (c bool true) = (c bool false)
           CP : changed assert false in a more informative error
        *)
-      errorlabstrm "Equality.construct_discriminator"
+      user_err "Equality.construct_discriminator"
 	(str "Cannot discriminate on inductive constructors with \
 		 dependent types.") in
   let (indp,_) = dest_ind_family indf in
@@ -974,7 +974,7 @@ let apply_on_clause (f,t) clause =
   let argmv =
     (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
-     | _  -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
+     | _  -> user_err "" (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
 
 let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn =
@@ -1052,7 +1052,7 @@ let discrEverywhere with_evars =
      else (* <= 8.2 compat *)
        tryAllHypsAndConcl (discrSimpleClause with_evars))
 (*    (fun gls ->
-       errorlabstrm "DiscrEverywhere" (str"No discriminable equalities."))
+       user_err "DiscrEverywhere" (str"No discriminable equalities."))
 *)
 let discr_tac with_evars = function
   | None -> discrEverywhere with_evars
@@ -1725,7 +1725,7 @@ let subst_one_var dep_proof_ok x =
           let hyps = Proofview.Goal.hyps gl in
           let test hyp _ = is_eq_x gl x hyp in
           Context.Named.fold_outside test ~init:() hyps;
-          errorlabstrm "Subst"
+          user_err "Subst"
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	       str".")
         with FoundHyp res -> res in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 8f3eb5eb5..e706316d7 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -632,7 +632,7 @@ let current_pure_db () =
   List.map snd (Hintdbmap.bindings (Hintdbmap.remove "v62" !searchtable))
 
 let error_no_such_hint_database x =
-  errorlabstrm "Hints" (str "No such Hint database: " ++ str x ++ str ".")
+  user_err "Hints" (str "No such Hint database: " ++ str x ++ str ".")
 
 (**************************************************************************)
 (*                       Definition of the summary                        *)
@@ -774,7 +774,7 @@ let make_resolves env sigma flags pri poly ?name cr =
     [make_exact_entry env sigma pri poly ?name; make_apply_entry env sigma flags pri poly ?name]
   in
   if List.is_empty ents then
-    errorlabstrm "Hint"
+    user_err "Hint"
       (pr_lconstr c ++ spc() ++
         (if pi1 flags then str"cannot be used as a hint."
 	else str "can be used as a hint only for eauto."));
@@ -817,7 +817,7 @@ let make_mode ref m =
   let n = List.length ctx in
   let m' = Array.of_list m in
     if not (n == Array.length m') then
-      errorlabstrm "Hint"
+      user_err "Hint"
 	(pr_global ref ++ str" has " ++ int n ++ 
 	   str" arguments while the mode declares " ++ int (Array.length m'))
     else m'
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 6e24cc469..aee3bc45d 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -450,7 +450,7 @@ let find_this_eq_data_decompose gl eqn =
     try (*first_match (match_eq eqn) inversible_equalities*)
       find_eq_data eqn
     with PatternMatchingFailure ->
-      errorlabstrm "" (str "No primitive equality found.") in
+      user_err "" (str "No primitive equality found.") in
   let eq_args =
     try extract_eq_args gl eq_args
     with PatternMatchingFailure ->
diff --git a/tactics/inv.ml b/tactics/inv.ml
index bda16b01c..a7f5ded5b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -76,7 +76,7 @@ let make_inv_predicate env evd indf realargs id status concl =
 	    (hyps_arity,concl)
       | Dep dflt_concl ->
 	  if not (occur_var env id concl) then
-	    errorlabstrm "make_inv_predicate"
+	    user_err "make_inv_predicate"
               (str "Current goal does not depend on " ++ pr_id id ++ str".");
           (* We abstract the conclusion of goal with respect to
              realargs and c to * be concl in order to rewrite and have
@@ -440,7 +440,7 @@ let raw_inversion inv_kind id status names =
       try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c)
       with UserError _ ->
         let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in
-        CErrors.errorlabstrm "" msg
+        CErrors.user_err "" msg
     in
     let IndType (indf,realargs) = find_rectype env sigma t in
     let evdref = ref sigma in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 642bf520b..e83093b0c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -183,7 +183,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let ind =
     try find_rectype env sigma i
     with Not_found ->
-      errorlabstrm "inversion_scheme" (no_inductive_inconstr env sigma i)
+      user_err "inversion_scheme" (no_inductive_inconstr env sigma i)
   in
   let (invEnv,invGoal) =
     compute_first_inversion_scheme env sigma ind sort dep_option
@@ -193,7 +193,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
        (global_vars env invGoal)
        (ids_of_named_context (named_context invEnv)));
   (*
-    errorlabstrm "lemma_inversion"
+    user_err "lemma_inversion"
     (str"Computed inversion goal was not closed in initial signature.");
   *)
   let pf = Proof.start (Evd.from_ctx (evar_universe_context sigma)) [invEnv,invGoal] in
@@ -248,7 +248,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
     add_inversion_lemma na env sigma c sort bool tac
   with
     |   UserError ("Case analysis",s) -> (* Reference to Indrec *)
-	  errorlabstrm "Inv needs Nodep Prop Set" s
+	  user_err "Inv needs Nodep Prop Set" s
 
 (* ================================= *)
 (* Applying a given inversion lemma  *)
@@ -261,10 +261,10 @@ let lemInv id c gls =
     Proofview.V82.of_tactic (Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) ~with_evars:false) gls
   with
     | NoSuchBinding ->
-	errorlabstrm ""
+	user_err ""
 	  (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
     | UserError (a,b) ->
-	 errorlabstrm "LemInv"
+	 user_err "LemInv"
 	   (str "Cannot refine current goal with the lemma " ++
 	      pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 28a7b634c..c9af1f11c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -643,7 +643,7 @@ module New = struct
 	    | Var id -> string_of_id id
 	    | _ -> "\b"
 	  in
-	  errorlabstrm "Tacticals.general_elim_then_using"
+	  user_err "Tacticals.general_elim_then_using"
             (str "The elimination combinator " ++ str name_elim ++ str " is unknown.")
     in
     let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ef66e6146..16643b6a7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -183,7 +183,7 @@ let introduction ?(check=true) id =
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
     let () = if check && mem_named_context id hyps then
-      errorlabstrm "Tactics.introduction"
+      user_err "Tactics.introduction"
         (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
     match kind_of_term (whd_evar sigma concl) with
@@ -255,7 +255,7 @@ let clear_dependency_msg env sigma id = function
       Printer.pr_existential env sigma ev ++ str"."
 
 let error_clear_dependency env sigma id err =
-  errorlabstrm "" (clear_dependency_msg env sigma id err)
+  user_err "" (clear_dependency_msg env sigma id err)
 
 let replacing_dependency_msg env sigma id = function
   | Evarutil.OccurHypInSimpleClause None ->
@@ -269,7 +269,7 @@ let replacing_dependency_msg env sigma id = function
       Printer.pr_existential env sigma ev ++ str"."
 
 let error_replacing_dependency env sigma id err =
-  errorlabstrm "" (replacing_dependency_msg env sigma id err)
+  user_err "" (replacing_dependency_msg env sigma id err)
 
 (* This tactic enables the user to remove hypotheses from the signature.
  * Some care is taken to prevent him from removing variables that are
@@ -350,7 +350,7 @@ let rename_hyp repl =
       let () =
         try
           let elt = Id.Set.choose (Id.Set.inter dst mods) in
-          CErrors.errorlabstrm "" (pr_id elt ++ str " is already used")
+          CErrors.user_err "" (pr_id elt ++ str " is already used")
         with Not_found -> ()
       in
       (** All is well *)
@@ -508,7 +508,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
     if not (eq_mind sp sp') then
       error "Fixpoints should be on the same mutual inductive declaration.";
     if mem_named_context f (named_context_of_val sign) then
-      errorlabstrm "Logic.prim_refiner"
+      user_err "Logic.prim_refiner"
         (str "Name " ++ pr_id f ++ str " already used in the environment");
     mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
   in
@@ -599,7 +599,7 @@ let pf_reduce_decl redfun where decl gl =
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str " has no value.");
+	user_err "" (pr_id id ++ str " has no value.");
       LocalAssum (id,redfun' ty)
   | LocalDef (id,b,ty) ->
       let b' = if where != InHypTypeOnly then redfun' b else b in
@@ -700,7 +700,7 @@ let pf_e_reduce_decl redfun where decl gl =
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str " has no value.");
+	user_err "" (pr_id id ++ str " has no value.");
     let Sigma (ty', sigma, p) = redfun sigma ty in
     Sigma (LocalAssum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
@@ -740,7 +740,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
   match decl with
   | LocalAssum (id,ty) ->
       if where == InHypValueOnly then
-	errorlabstrm "" (pr_id id ++ str " has no value.");
+	user_err "" (pr_id id ++ str " has no value.");
     let Sigma (ty', sigma, p) = (redfun false).e_redfun env sigma ty in
     Sigma (LocalAssum (id, ty'), sigma, p)
   | LocalDef (id,b,ty) ->
@@ -778,12 +778,12 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
         isSort (whd_all env sigma t2)
       then (mayneedglobalcheck := true; sigma)
       else
-        errorlabstrm "convert-check-hyp" (str "Types are incompatible.")
+        user_err "convert-check-hyp" (str "Types are incompatible.")
     else sigma
   end
   else
     if not (isSort (whd_all env sigma t1)) then
-      errorlabstrm "convert-check-hyp" (str "Not a type.")
+      user_err "convert-check-hyp" (str "Not a type.")
     else sigma
 
 (* Now we introduce different instances of the previous tacticals *)
@@ -792,7 +792,7 @@ let change_and_check cv_pb mayneedglobalcheck deep t = { e_redfun = begin fun en
   let sigma = Sigma.to_evar_map sigma in
   let sigma = check_types env sigma mayneedglobalcheck deep t' c in
   let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
-  if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
+  if not b then user_err "convert-check-hyp" (str "Not convertible.");
   Sigma.Unsafe.of_pair (t', sigma)
 end }
 
@@ -883,7 +883,7 @@ let reduce redexp cl =
 let unfold_constr = function
   | ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp]
   | VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id]
-  | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.")
+  | _ -> user_err "unfold_constr" (str "Cannot unfold a non-constant.")
 
 (*******************************************)
 (*         Introduction tactics            *)
@@ -1078,7 +1078,7 @@ let depth_of_quantified_hypothesis red h gl =
   match lookup_hypothesis_as_renamed_gen red h gl with
     | Some depth -> depth
     | None ->
-        errorlabstrm "lookup_quantified_hypothesis"
+        user_err "lookup_quantified_hypothesis"
           (str "No " ++ msg_quantified_hypothesis h ++
 	  strbrk " in current goal" ++
 	  (if red then strbrk " even after head-reduction" else mt ()) ++
@@ -1227,7 +1227,7 @@ let cut c =
 let error_uninstantiated_metas t clenv =
   let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
   let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta")
-  in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
+  in user_err "" (str "Cannot find an instance for " ++ pr_id id ++ str".")
 
 let check_unresolved_evars_of_metas sigma clenv =
   (* This checks that Metas turned into Evars by *)
@@ -1360,7 +1360,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
   let indmv =
     (match kind_of_term (nth_arg i elimclause.templval.rebus) with
        | Meta mv -> mv
-       | _  -> errorlabstrm "elimination_clause"
+       | _  -> user_err "elimination_clause"
              (str "The type of elimination clause is not well-formed."))
   in
   let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
@@ -1525,7 +1525,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
     try match List.remove Int.equal indmv (clenv_independent elimclause) with
       | [a] -> a
       | _ -> failwith ""
-    with Failure _ -> errorlabstrm "elimination_clause"
+    with Failure _ -> user_err "elimination_clause"
           (str "The type of elimination clause is not well-formed.") in
   let elimclause'  = clenv_fchain ~flags indmv elimclause indclause in
   let hyp = mkVar id in
@@ -1534,7 +1534,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
   let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
   let new_hyp_typ  = clenv_type elimclause'' in
   if Term.eq_constr hyp_typ new_hyp_typ then
-    errorlabstrm "general_rewrite_in"
+    user_err "general_rewrite_in"
       (str "Nothing to rewrite in " ++ pr_id id ++ str".");
   clenv_refine_in with_evars id id sigma elimclause''
     (fun id -> Proofview.tclUNIT ())
@@ -2015,7 +2015,7 @@ let clear_body ids =
     let map = function
     | LocalAssum (id,t) as decl ->
       let () = if List.mem_f Id.equal id ids then
-        errorlabstrm "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
+        user_err "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition")
       in
       decl
     | LocalDef (id,_,t) as decl ->
@@ -2146,7 +2146,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
   if Int.equal i 0 then error "The constructors are numbered starting from 1.";
   begin match expctdnumopt with
     | Some n when not (Int.equal n nconstr) ->
-	errorlabstrm "Tactics.check_number_of_constructors"
+	user_err "Tactics.check_number_of_constructors"
           (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
     | _ -> ()
   end;
@@ -2725,7 +2725,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t
 let generalized_name c t ids cl = function
   | Name id as na ->
       if Id.List.mem id ids then
-	errorlabstrm "" (pr_id id ++ str " is already used.");
+	user_err "" (pr_id id ++ str " is already used.");
       na
   | Anonymous ->
       match kind_of_term c with
@@ -2886,7 +2886,7 @@ let specialize (c,lbind) ipat =
       let tstack = chk tstack in
       let term = applist(thd,List.map (nf_evar clause.evd) tstack) in
       if occur_meta term then
-	errorlabstrm "" (str "Cannot infer an instance for " ++
+	user_err "" (str "Cannot infer an instance for " ++
 
           pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++
 	  str ".");
@@ -2931,7 +2931,7 @@ let unfold_body x =
   (** We normalize the given hypothesis immediately. *)
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
   let xval = match Context.Named.lookup x hyps with
-  | LocalAssum _ -> errorlabstrm "unfold_body"
+  | LocalAssum _ -> user_err "unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
   | LocalDef (_,xval,_) -> xval
   in
@@ -3428,7 +3428,7 @@ let make_up_names n ind_opt cname =
 
 let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
-  errorlabstrm "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
+  user_err "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
 
 let glob = Universes.constr_of_global
 
@@ -4046,7 +4046,7 @@ let recolle_clenv i params args elimclause gl =
       (fun x ->
 	match kind_of_term x with
 	  | Meta mv -> mv
-	  | _  -> errorlabstrm "elimination_clause"
+	  | _  -> user_err "elimination_clause"
               (str "The type of the elimination clause is not well-formed."))
       arr in
   let k = match i with -1 -> Array.length lindmv - List.length args | _ -> i in
@@ -4193,7 +4193,7 @@ let clear_unselected_context id inhyps cls =
   let open Context.Named.Declaration in
   if occur_var (Tacmach.New.pf_env gl) id (Tacmach.New.pf_concl gl) &&
     cls.concl_occs == NoOccurrences
-  then errorlabstrm ""
+  then user_err ""
     (str "Conclusion must be mentioned: it depends on " ++ pr_id id
      ++ str ".");
   match cls.onhyps with
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 180b836ea..d6c2ccad2 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -340,7 +340,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
     let rec find i =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
-            else errorlabstrm "AutoIndDecl.do_replace_lb"
+            else user_err "AutoIndDecl.do_replace_lb"
                    (str "Var " ++ pr_id s ++ str " seems unknown.")
       )
     in mkVar (find 1)
@@ -398,7 +398,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
     let rec find i =
       if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
-            else errorlabstrm "AutoIndDecl.do_replace_bl"
+            else user_err "AutoIndDecl.do_replace_bl"
                    (str "Var " ++ pr_id s ++ str " seems unknown.")
       )
     in mkVar (find 1)
@@ -506,7 +506,7 @@ let eqI ind l =
                            (List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
   and e, eff = 
     try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff 
-    with Not_found -> errorlabstrm "AutoIndDecl.eqI"
+    with Not_found -> user_err "AutoIndDecl.eqI"
       (str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed.");
   in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff
 
@@ -633,7 +633,7 @@ let side_effect_of_mode = function
 let make_bl_scheme mode mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
-    errorlabstrm ""
+    user_err ""
       (str "Automatic building of boolean->Leibniz lemmas not supported");
   let ind = (mind,0) in
   let nparams = mib.mind_nparams in
@@ -756,7 +756,7 @@ let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
 let make_lb_scheme mode mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
-    errorlabstrm ""
+    user_err ""
       (str "Automatic building of Leibniz->boolean lemmas not supported");
   let ind = (mind,0) in
   let nparams = mib.mind_nparams in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 6d53ec9d8..bf17867e8 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -98,7 +98,7 @@ let class_of_global = function
   | IndRef sp -> CL_IND sp
   | VarRef id -> CL_SECVAR id
   | ConstructRef _ as c ->
-      errorlabstrm "class_of_global"
+      user_err "class_of_global"
 	(str "Constructors, such as " ++ Printer.pr_global c ++
 	   str ", cannot be used as a class.")
 
@@ -177,7 +177,7 @@ let ident_key_of_class = function
 (* Identity coercion *)
 
 let error_not_transparent source =
-  errorlabstrm "build_id_coercion"
+  user_err "build_id_coercion"
     (pr_class source ++ str " must be a transparent constant.")
 
 let build_id_coercion idf_opt source poly =
@@ -208,7 +208,7 @@ let build_id_coercion idf_opt source poly =
       (Reductionops.is_conv_leq env sigma
 	(Typing.unsafe_type_of env sigma val_f) typ_f)
     then
-      errorlabstrm "" (strbrk
+      user_err "" (strbrk
 	"Cannot be defined as coercion (maybe a bad number of arguments).")
   in
   let idf =
@@ -284,7 +284,7 @@ let add_new_coercion_core coef stre poly source target isid =
 let try_add_new_coercion_core ref ~local c d e f =
   try add_new_coercion_core ref (loc_of_bool local) c d e f
   with CoercionError e ->
-      errorlabstrm "try_add_new_coercion_core"
+      user_err "try_add_new_coercion_core"
         (explain_coercion_error ref e ++ str ".")
 
 let try_add_new_coercion ref ~local poly =
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 26cb7451a..6d62ce24a 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -169,7 +169,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 	Name id ->
 	  let sp = Lib.make_path id in
 	    if Nametab.exists_cci sp then
-	      errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
+	      user_err "new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
 	    id
       | Anonymous ->
 	  let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b9a72fa33..4d333c30d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1312,7 +1312,7 @@ let do_program_fixpoint local poly l =
 	  match n with
 	  | Some n -> mkIdentC (snd n)
 	  | None ->
-	      errorlabstrm "do_program_fixpoint"
+	      user_err "do_program_fixpoint"
 		(str "Recursive argument required for well-founded fixpoints")
 	in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
 	     
@@ -1326,7 +1326,7 @@ let do_program_fixpoint local poly l =
 	  do_program_recursive local poly fixkind fixl ntns
 
     | _, _ ->
-	errorlabstrm "do_program_fixpoint"
+	user_err "do_program_fixpoint"
 	  (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
 let check_safe () =
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index d9cd574a0..b90e62048 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -136,7 +136,7 @@ let get_compat_version = function
   | "8.3" -> Flags.V8_3
   | "8.2" -> Flags.V8_2
   | ("8.1" | "8.0") as s ->
-    CErrors.errorlabstrm "get_compat_version"
+    CErrors.user_err "get_compat_version"
       (str "Compatibility with version " ++ str s ++ str " not supported.")
-  | s -> CErrors.errorlabstrm "get_compat_version"
+  | s -> CErrors.user_err "get_compat_version"
       (str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 6d57a21dc..fee5cffeb 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -87,7 +87,7 @@ let declare_scheme_object s aux f =
   try
     let _ = Hashtbl.find scheme_object_table key in
 (*    let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
-    errorlabstrm "IndTables.declare_scheme_object"
+    user_err "IndTables.declare_scheme_object"
       (str "Scheme object " ++ str key ++ str " already declared.")
   with Not_found ->
     Hashtbl.add scheme_object_table key (s,f);
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index 154f787ef..7664acbb6 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -18,7 +18,7 @@ let check_locality locality_flag =
   match locality_flag with
   | Some b ->
     let s = if b then "Local" else "Global" in
-    CErrors.errorlabstrm "Locality.check_locality"
+    CErrors.user_err "Locality.check_locality"
       (str "This command does not support the \"" ++ str s ++ str "\" prefix.")
   | None -> ()
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a1edb7139..cef074699 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -238,7 +238,7 @@ let rec find_pattern nt xl = function
   | _, Break s :: _ | Break s :: _, _ ->
       error ("A break occurs on one side of \"..\" but not on the other side.")
   | _, Terminal s :: _ | Terminal s :: _, _ ->
-      errorlabstrm "Metasyntax.find_pattern"
+      user_err "Metasyntax.find_pattern"
         (str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
   | _, [] ->
       error msg_expected_form_of_recursive_notation
@@ -300,7 +300,7 @@ let rec get_notation_vars = function
       let vars = get_notation_vars sl in
       if Id.equal id ldots_var then vars else
 	if Id.List.mem id vars then
-	  errorlabstrm "Metasyntax.get_notation_vars"
+	  user_err "Metasyntax.get_notation_vars"
             (str "Variable " ++ pr_id id ++ str " occurs more than once.")
 	else
           id::vars
@@ -314,7 +314,7 @@ let analyze_notation_tokens l =
   recvars, List.subtract Id.equal vars (List.map snd recvars), l
 
 let error_not_same_scope x y =
-  errorlabstrm "Metasyntax.error_not_name_scope"
+  user_err "Metasyntax.error_not_name_scope"
     (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.")
 
 (**********************************************************************)
@@ -390,7 +390,7 @@ let check_open_binder isopen sl m =
   | _ -> assert false
   in
   if isopen && not (List.is_empty sl) then
-    errorlabstrm "" (str "as " ++ pr_id m ++
+    user_err "" (str "as " ++ pr_id m ++
       str " is a non-closed binder, no such \"" ++
       prlist_with_sep spc pr_token sl
       ++ strbrk "\" is allowed to occur.")
@@ -661,7 +661,7 @@ let pr_level ntn (from,args) =
   prlist_with_sep pr_comma (pr_arg_level from) args
 
 let error_incompatible_level ntn oldprec prec =
-  errorlabstrm ""
+  user_err ""
     (str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++
     pr_level ntn oldprec ++
     spc() ++ str "while it is now required to be" ++ spc() ++
@@ -731,7 +731,7 @@ let interp_modifiers modl =
     | SetEntryType (s,typ) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id etyps then
-	  errorlabstrm "Metasyntax.interp_modifiers"
+	  user_err "Metasyntax.interp_modifiers"
             (str s ++ str " is already assigned to an entry or constr level.");
 	interp assoc level ((id,typ)::etyps) format extra l
     | SetItemLevel ([],n) :: l ->
@@ -739,7 +739,7 @@ let interp_modifiers modl =
     | SetItemLevel (s::idl,n) :: l ->
 	let id = Id.of_string s in
 	if Id.List.mem_assoc id etyps then
-	  errorlabstrm "Metasyntax.interp_modifiers"
+	  user_err "Metasyntax.interp_modifiers"
             (str s ++ str " is already assigned to an entry or constr level.");
 	let typ = ETConstr (n,()) in
 	interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l)
@@ -770,7 +770,7 @@ let check_infix_modifiers modifiers =
 let check_useless_entry_types recvars mainvars etyps =
   let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
   match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with
-  | (x,_)::_ -> errorlabstrm "Metasyntax.check_useless_entry_types"
+  | (x,_)::_ -> user_err "Metasyntax.check_useless_entry_types"
                   (pr_id x ++ str " is unbound in the notation.")
   | _ -> ()
 
@@ -813,7 +813,7 @@ let join_auxiliary_recursive_types recvars etyps =
     | None, Some ytyp -> (x,ytyp)::typs
     | Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *)
     | Some xtyp, Some ytyp ->
-	errorlabstrm ""
+	user_err ""
 	  (strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++
 	   strbrk ", both ends have incompatible types."))
     recvars etyps
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index fbd1e6033..c74c3522d 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -124,13 +124,13 @@ let ml_load s =
         | (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e)
         | exc ->
             let msg = report_on_load_obj_error exc in
-            errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
+            user_err "Mltop.load_object" (str"Cannot link ml-object " ++
                   str s ++ str" to Coq code (" ++ msg ++ str ")."))
     | WithoutTop ->
         try
           Dynlink.loadfile s; s
 	with Dynlink.Error a ->
-          errorlabstrm "Mltop.load_object"
+          user_err "Mltop.load_object"
             (strbrk "while loading " ++ str s ++
              strbrk ": " ++ str (Dynlink.error_message a))
 
@@ -151,7 +151,7 @@ let dir_ml_use s =
 	 if Dynlink.is_native then " Loading ML code works only in bytecode."
 	 else ""
        in
-      errorlabstrm "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
+      user_err "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
 
 (* Adds a path to the ML paths *)
 let add_ml_dir s =
@@ -221,7 +221,7 @@ let get_ml_object_suffix name =
 let file_of_name name =
   let suffix = get_ml_object_suffix name in
   let fail s =
-    errorlabstrm "Mltop.load_object"
+    user_err "Mltop.load_object"
       (str"File not found on loadpath : " ++ str s ++ str"\n" ++
        str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in
   if not (Filename.is_relative name) then
@@ -355,7 +355,7 @@ let trigger_ml_object verb cache reinit ?path name =
     add_loaded_module name (known_module_path name);
     if cache then perform_cache_obj name
   end else if not has_dynlink then
-    errorlabstrm "Mltop.trigger_ml_object"
+    user_err "Mltop.trigger_ml_object"
       (str "Dynamic link not supported (module " ++ str name ++ str ")")
   else begin
     let file = file_of_name (Option.default name path) in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 38d4a62b4..b9fd2894d 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -258,7 +258,7 @@ let safe_init_constant md name () =
   Coqlib.gen_constant "Obligations" md name
 let hide_obligation = safe_init_constant tactics_module "obligation"
 
-let pperror cmd = CErrors.errorlabstrm "Program" cmd
+let pperror cmd = CErrors.user_err "Program" cmd
 let error s = pperror (str s)
 
 let reduce c =
@@ -398,7 +398,7 @@ let rec prod_app t n =
     | Prod (_,_,b) -> subst1 n b
     | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
     | _ ->
-	errorlabstrm "prod_app"
+	user_err "prod_app"
 	  (str"Needed a product, but didn't find one" ++ fnl ())
 
 
@@ -444,7 +444,7 @@ let from_prg : program_info ProgMap.t ref =
 let close sec =
   if not (ProgMap.is_empty !from_prg) then
     let keys = map_keys !from_prg in
-      errorlabstrm "Program" 
+      user_err "Program" 
 	(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
 	   prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
 	   (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++
@@ -718,7 +718,7 @@ let get_prog name =
                 let progs = Id.Set.elements (ProgMap.domain prg_infos) in
                 let prog = List.hd progs in
                 let progs = prlist_with_sep pr_comma Nameops.pr_id progs in
-                errorlabstrm ""
+                user_err ""
                   (str "More than one program with unsolved obligations: " ++ progs
                   ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\""))
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 6a64b0d66..22dc8c957 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -208,7 +208,7 @@ let warning_or_error coe indsp err =
 	  | _ ->
               (pr_id fi ++ strbrk " cannot be defined because it is not typable.")
   in
-  if coe then errorlabstrm "structure" st;
+  if coe then user_err "structure" st;
   Flags.if_verbose Feedback.msg_info (hov 0 st)
 
 type field_status =
@@ -235,7 +235,7 @@ let subst_projection fid l c =
 	    | Projection t -> lift depth t
 	    | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
 	    | NoProjection Anonymous ->
-                errorlabstrm "" (str "Field " ++ pr_id fid ++
+                user_err "" (str "Field " ++ pr_id fid ++
                   str " depends on the " ++ pr_nth (k-depth-1) ++ str
                   " field which has no name.")
         else
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3f784fd8a..9e3494145 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -483,7 +483,7 @@ let vernac_start_proof locality p kind l lettop =
 	| None -> ()) l;
   if not(refining ()) then
     if lettop then
-      errorlabstrm "Vernacentries.StartProof"
+      user_err "Vernacentries.StartProof"
 	(str "Let declarations can only be used in proof editing mode.");
   start_proof_and_print (local, p, Proof kind) l no_hook
 
@@ -855,7 +855,7 @@ let vernac_set_used_variables e =
   let vars = Environ.named_context env in
   List.iter (fun id -> 
     if not (List.exists (Id.equal id % get_id) vars) then
-      errorlabstrm "vernac_set_used_variables"
+      user_err "vernac_set_used_variables"
         (str "Unknown variable: " ++ pr_id id))
     l;
   let _, to_clear = set_used_variables l in
@@ -974,9 +974,9 @@ let vernac_declare_arguments locality r l nargs flags =
     | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls
     | [], _::_, (Some _)::ls when extra_scope_flag ->
        error "Extra notation scopes can be set on anonymous arguments only"
-    | [], x::_, _ -> errorlabstrm "vernac_declare_arguments"
+    | [], x::_, _ -> user_err "vernac_declare_arguments"
                        (str "Extra argument " ++ pr_name x ++ str ".")
-    | l, [], _ -> errorlabstrm "vernac_declare_arguments"
+    | l, [], _ -> user_err "vernac_declare_arguments"
                     (str "The following arguments are not declared: " ++
                        prlist_with_sep pr_comma pr_name l ++ str ".")
     | _::li, _::ld, _::ls -> check li ld ls 
@@ -1019,7 +1019,7 @@ let vernac_declare_arguments locality r l nargs flags =
       let sr', impl = List.fold_map (fun b -> function
         | (Anonymous, _,_, true, max), Name id -> assert false
         | (Name x, _,_, true, _), Anonymous ->
-            errorlabstrm "vernac_declare_arguments"
+            user_err "vernac_declare_arguments"
               (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.")
         | (Name iid, _,_, true, max), Name id ->
            set_renamed iid id;
@@ -1033,7 +1033,7 @@ let vernac_declare_arguments locality r l nargs flags =
       some_renaming_specified l in
   if some_renaming_specified then
     if not (List.mem `Rename flags) then
-      errorlabstrm "vernac_declare_arguments"
+      user_err "vernac_declare_arguments"
         (str "To rename arguments the \"rename\" flag must be specified." ++
            match !renamed_arg with
            | None -> mt ()
@@ -1077,7 +1077,7 @@ let vernac_declare_arguments locality r l nargs flags =
     | ConstRef _ as c ->
        Reductionops.ReductionBehaviour.set
          (make_section_locality locality) c (rargs, nargs, flags)
-    | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
+    | _ -> user_err "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
   end;
   if not (some_renaming_specified ||
           some_implicits_specified ||
@@ -1498,7 +1498,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
       | Some n,AN (Ident (_loc,id)) ->  (* goal number given, catch if wong *)
 	 (try get_nth_goal n,id
 	  with
-	    Failure _ -> errorlabstrm "print_about_hyp_globs"
+	    Failure _ -> user_err "print_about_hyp_globs"
                            (str "No such goal: " ++ int n ++ str "."))
       | _ , _ -> raise NoHyp in
     let hyps = pf_hyps gl in
@@ -1597,7 +1597,7 @@ let interp_search_about_item env =
 	    (fun _ -> true) s sc in
 	GlobSearchSubPattern (Pattern.PRef ref)
       with UserError _ ->
-	errorlabstrm "interp_search_about_item"
+	user_err "interp_search_about_item"
           (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
 
 let vernac_search s gopt r =
@@ -1877,12 +1877,12 @@ let interp ?proof ~loc locality poly c =
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
 
   (* The STM should handle that, but LOAD bypasses the STM... *)
-  | VernacAbort id -> CErrors.errorlabstrm "" (str "Abort cannot be used through the Load command")
-  | VernacAbortAll -> CErrors.errorlabstrm "" (str "AbortAll cannot be used through the Load command")
-  | VernacRestart -> CErrors.errorlabstrm "" (str "Restart cannot be used through the Load command")
-  | VernacUndo _ -> CErrors.errorlabstrm "" (str "Undo cannot be used through the Load command")
-  | VernacUndoTo _ -> CErrors.errorlabstrm "" (str "UndoTo cannot be used through the Load command")
-  | VernacBacktrack _ -> CErrors.errorlabstrm "" (str "Backtrack cannot be used through the Load command")
+  | VernacAbort id -> CErrors.user_err "" (str "Abort cannot be used through the Load command")
+  | VernacAbortAll -> CErrors.user_err "" (str "AbortAll cannot be used through the Load command")
+  | VernacRestart -> CErrors.user_err "" (str "Restart cannot be used through the Load command")
+  | VernacUndo _ -> CErrors.user_err "" (str "Undo cannot be used through the Load command")
+  | VernacUndoTo _ -> CErrors.user_err "" (str "UndoTo cannot be used through the Load command")
+  | VernacBacktrack _ -> CErrors.user_err "" (str "Backtrack cannot be used through the Load command")
   
   (* Proof management *)
   | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
@@ -2014,7 +2014,7 @@ let with_fail b f =
       let (e, _) = CErrors.push e in
       match e with
       | HasNotFailed ->
-          errorlabstrm "Fail" (str "The command has not failed!")
+          user_err "Fail" (str "The command has not failed!")
       | HasFailed msg ->
           if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info
             (str "The command has indeed failed with message:" ++ fnl () ++ msg)
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index d81e3d6b5..147727e7c 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -22,7 +22,7 @@ let vinterp_add depr s f =
   try
     Hashtbl.add vernac_tab s (depr, f)
   with Failure _ ->
-    errorlabstrm "vinterp_add"
+    user_err "vinterp_add"
       (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
 
 let overwriting_vinterp_add s f =
@@ -37,7 +37,7 @@ let vinterp_map s =
   try
     Hashtbl.find vernac_tab s
   with Failure _ | Not_found ->
-    errorlabstrm "Vernac Interpreter"
+    user_err "Vernac Interpreter"
       (str"Cannot find vernac command " ++ str (fst s) ++ str".")
 
 let vinterp_init () = Hashtbl.clear vernac_tab
author	Emilio Jesus Gallego Arias <e+git@x80.org>	2016-08-19 01:58:04 +0200
committer	Emilio Jesus Gallego Arias <e+git@x80.org>	2016-08-19 02:01:56 +0200
commit	543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (patch)
tree	caf22d0e607ed9e0bf9ba64d76b4c2aebce63d5a
parent	de038270f72214b169d056642eb7144a79e6f126 (diff)