Make the user_err header an optional parameter.

Suggested by @ppedrot

116 files changed, 458 insertions, 451 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 38d2057eb..8565e96fc 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
-  user_err "load_absolute_library_from"
+  user_err ~hdr:"load_absolute_library_from"
     (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++
      str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ())
 
 let error_lib_not_found qid =
-  user_err "load_absolute_library_from"
+  user_err ~hdr:"load_absolute_library_from"
     (str"Cannot find library " ++ pr_path qid ++ str" in loadpath")
 
 let try_locate_absolute_library dir =
@@ -313,18 +313,18 @@ let intern_from_file (dir, f) =
       let () = close_in ch in
       let ch = open_in_bin f in
       if not (String.equal (Digest.channel ch pos) checksum) then
-        user_err "intern_from_file" (str "Checksum mismatch");
+        user_err ~hdr:"intern_from_file" (str "Checksum mismatch");
       let () = close_in ch in
       if dir <> sd.md_name then
-        user_err "intern_from_file"
+        user_err ~hdr:"intern_from_file"
           (name_clash_message dir sd.md_name f);
       if tasks <> None || discharging <> None then
-        user_err "intern_from_file"
+        user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " contains unfinished tasks");
       if opaque_csts <> None then begin
        Feedback.msg_notice(str " (was a vio file) ");
       Option.iter (fun (_,_,b) -> if not b then
-        user_err "intern_from_file"
+        user_err ~hdr:"intern_from_file"
           (str "The file "++str f++str " is still a .vio"))
         opaque_csts;
       Validate.validate !Flags.debug Values.v_univopaques opaque_csts;
diff --git a/checker/checker.ml b/checker/checker.ml
index 0c411ae44..06d0cd1c0 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -213,7 +213,9 @@ let report () = (str "." ++ spc () ++ str "Please report.")
 
 let guill s = str "\"" ++ str s ++ str "\""
 
-let where s =
+let where = function
+| None -> mt ()
+| Some s ->
   if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
 let rec explain_exn = function
diff --git a/checker/modops.ml b/checker/modops.ml
index de1db6e35..aba9da2fe 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -33,7 +33,7 @@ let error_no_such_label_sub l l1 =
          Label.to_string l^" is missing in "^l1^".")
 
 let error_not_a_module_loc loc s =
-  user_err ~loc "" (str ("\""^Label.to_string s^"\" is not a module"))
+  user_err ~loc  (str ("\""^Label.to_string s^"\" is not a module"))
 
 let error_not_a_module s = error_not_a_module_loc Loc.ghost s
 
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index c0b3a3e73..f7cd4d6f6 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 (user_err"unsafe_import") clib.comp_name env clib.comp_deps;
+  else check_imports (user_err (str "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 699130944..7d5e3d1fe 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -12,6 +12,8 @@
 
 - `errorlabstrm` has been removed in favor of `user_err`.
 
+- The header parameter to `user_err` has been made optional.
+
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
diff --git a/engine/evd.ml b/engine/evd.ml
index 7ee342ea0..15654b4c6 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -383,7 +383,7 @@ let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) =
   | Misctypes.IntroAnonymous -> None
   | Misctypes.IntroIdentifier id ->
     if Idmap.mem id idtoev then
-    user_err "" (str "Already an existential evar of name " ++ pr_id id);
+    user_err  (str "Already an existential evar of name " ++ pr_id id);
     Some id
   | Misctypes.IntroFresh id ->
     let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index e14a2bd39..6e821ea5a 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.user_err "Some timeout function" (Pp.str"Timeout!")
+  | Timeout -> CErrors.user_err ~hdr:"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 c47c44e22..51b3a7260 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.user_err ""
+    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.user_err "" errmsg
+      CErrors.user_err  errmsg
   | _ -> raise CErrors.Unhandled
 end
 
@@ -845,11 +845,11 @@ let tclPROGRESS t =
   if not test then
     tclUNIT res
   else
-    tclZERO (CErrors.UserError ("Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
+    tclZERO (CErrors.UserError (Some "Proofview.tclPROGRESS" , Pp.str"Failed to progress."))
 
 exception Timeout
 let _ = CErrors.register_handler begin function
-  | Timeout -> CErrors.user_err "Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
+  | Timeout -> CErrors.user_err ~hdr:"Proofview.tclTIMEOUT" (Pp.str"Tactic timeout!")
   | _ -> Pervasives.raise CErrors.Unhandled
 end
 
diff --git a/engine/uState.ml b/engine/uState.ml
index c82c30400..c66af02bb 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -255,7 +255,7 @@ let universe_context ?names ctx =
           let l =
             try UNameMap.find (Id.to_string id) (fst ctx.uctx_names)
             with Not_found ->
-              user_err ~loc "universe_context"
+              user_err ~loc ~hdr:"universe_context"
                             (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.")
           in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc))
          pl ([], [], levels)
@@ -269,7 +269,7 @@ let universe_context ?names ctx =
              Option.default Loc.ghost info.uloc
            with Not_found -> Loc.ghost
          in
-           user_err ~loc "universe_context"
+           user_err ~loc ~hdr:"universe_context"
                         ((str(CString.plural n "Universe") ++ spc () ++
 			     Univ.LSet.pr (pr_uctx_level ctx) left ++
 			   spc () ++ str (CString.conjugate_verb_to_be n) ++
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index db0f96715..1d215f4ca 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -96,7 +96,7 @@ let is_undo cmd = match cmd with
 (** Check whether a command is forbidden by CoqIDE *)
 
 let coqide_cmd_checks (loc,ast) =
-  let user_error s = CErrors.user_err ~loc "CoqIde" (str s) in
+  let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in
   if is_debug ast then
     user_error "Debug mode not available within CoqIDE";
   if is_known_option ast then
@@ -300,7 +300,7 @@ let dirpath_of_string_list s =
   let id =
     try Nametab.full_name_module qid
     with Not_found ->
-      CErrors.user_err "Search.interface_search"
+      CErrors.user_err ~hdr:"Search.interface_search"
         (str "Module " ++ str path ++ str " not found.")
   in
   id
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 9097a56f8..59c24900d 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -382,18 +382,18 @@ let rec prod_constr_expr c = function
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
   | Qualid (loc,_) ->
-      CErrors.user_err ~loc "coerce_reference_to_id"
+      CErrors.user_err ~loc ~hdr:"coerce_reference_to_id"
         (str "This expression should be a simple identifier.")
 
 let coerce_to_id = function
   | CRef (Ident (loc,id),_) -> (loc,id)
   | a -> CErrors.user_err ~loc:(constr_loc a)
-       "coerce_to_id"
+       ~hdr:"coerce_to_id"
          (str "This expression should be a simple identifier.")
 
 let coerce_to_name = function
   | CRef (Ident (loc,id),_) -> (loc,Name id)
   | CHole (loc,_,_,_) -> (loc,Anonymous)
   | a -> CErrors.user_err
-         ~loc:(constr_loc a) "coerce_to_name"
+         ~loc:(constr_loc a) ~hdr:"coerce_to_name"
          (str "This expression should be a name.")
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3e6bc80f2..f7fcbb4ee 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -94,7 +94,7 @@ let is_record indsp =
 let encode_record r =
   let indsp = global_inductive r in
   if not (is_record indsp) then
-    user_err ~loc:(loc_of_reference r) "encode_record"
+    user_err ~loc:(loc_of_reference r) ~hdr:"encode_record"
       (str "This type is not a structure type.");
   indsp
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 82039abd3..48a32bf5e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -155,16 +155,16 @@ let explain_internalization_error e =
   in pp ++ str "."
 
 let error_bad_inductive_type ?loc =
-  user_err ?loc "" (str
+  user_err ?loc  (str
     "This should be an inductive type applied to patterns.")
 
 let error_parameter_not_implicit ?loc =
-  user_err ?loc "" (str
+  user_err ?loc  (str
    "The parameters do not bind in patterns;" ++ spc () ++ str
     "they must be replaced by '_'.")
 
 let error_ldots_var ?loc =
-  user_err ?loc "" (str "Special token " ++ pr_id ldots_var ++
+  user_err ?loc  (str "Special token " ++ pr_id ldots_var ++
     str " is for use in the Notation command.")
 
 (**********************************************************************)
@@ -263,13 +263,13 @@ let pr_scope_stack = function
       str "[" ++ prlist_with_sep pr_comma str l ++ str "]"
 
 let error_inconsistent_scope ?loc id scopes1 scopes2 =
-  user_err ?loc "set_var_scope"
+  user_err ?loc ~hdr:"set_var_scope"
    (pr_id id ++ str " is here used in " ++
     pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++
     pr_scope_stack scopes1)
 
 let error_expect_binder_notation_type ?loc id =
-  user_err ?loc ""
+  user_err ?loc 
    (pr_id id ++
     str " is expected to occur in binding position in the right-hand side.")
 
@@ -366,14 +366,14 @@ let check_hidden_implicit_parameters id impls =
     | (Inductive indparams,_,_,_) -> Id.List.mem id indparams
     | _ -> false) impls
   then
-    user_err "" (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 =
   function
   | loc,Anonymous ->
       if global_level then
-	user_err ~loc "" (str "Anonymous variables not allowed");
+	user_err ~loc  (str "Anonymous variables not allowed");
       env
   | loc,Name id ->
       check_hidden_implicit_parameters id env.impls ;
@@ -764,7 +764,7 @@ let string_of_ty = function
 let gvar (loc, id) us = match us with
 | None -> GVar (loc, id)
 | Some _ ->
-  user_err ~loc "" (str "Variable " ++ pr_id id ++
+  user_err ~loc  (str "Variable " ++ pr_id id ++
     str " cannot have a universe instance")
 
 let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
@@ -792,7 +792,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
     else gvar (loc,id) us, [], [], []
   else if Id.Set.mem id ltacvars.ltac_bound then
     (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
-    user_err ~loc "intern_var"
+    user_err ~loc ~hdr:"intern_var"
      (str "variable " ++ pr_id id ++ str " should be bound to a term.")
   else
     (* Is [id] a goal or section variable *)
@@ -825,7 +825,7 @@ let find_appl_head_data c =
   | x -> x,[],[],[]
 
 let error_not_enough_arguments loc =
-  user_err ~loc "" (str "Abbreviation is not applied enough.")
+  user_err ~loc  (str "Abbreviation is not applied enough.")
 
 let check_no_explicitation l =
   let is_unset (a, b) = match b with None -> false | Some _ -> true in
@@ -834,7 +834,7 @@ let check_no_explicitation l =
   | [] -> ()
   | (_, None) :: _ -> assert false
   | (_, Some (loc, _)) :: _ ->
-    user_err ~loc "" (str"Unexpected explicitation of the argument of an abbreviation.")
+    user_err ~loc  (str"Unexpected explicitation of the argument of an abbreviation.")
 
 let dump_extended_global loc = function
   | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob loc ref
@@ -872,7 +872,7 @@ let intern_qualid loc qid intern env lvar us args =
       | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
          GApp (loc, GRef (loc', ref, us), arg)
       | Some _, _ ->
-        user_err ~loc "" (str "Notation " ++ pr_qualid qid ++
+        user_err ~loc  (str "Notation " ++ pr_qualid qid ++
           str " cannot have a universe instance, its expanded head
                does not start with a reference")
       in
@@ -982,7 +982,7 @@ let check_number_of_pattern loc n l =
 
 let check_or_pat_variables loc ids idsl =
   if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then
-    user_err ~loc "" (str
+    user_err ~loc  (str
     "The components of this disjunctive pattern must bind the same variables.")
 
 (** Use only when params were NOT asked to the user.
@@ -1042,10 +1042,10 @@ let find_constructor loc add_params ref =
   | ConstructRef cstr -> cstr
   | IndRef _ ->
     let error = str "There is an inductive name deep in a \"in\" clause." in
-    user_err ~loc "find_constructor" error
+    user_err ~loc ~hdr:"find_constructor" error
   | ConstRef _ | VarRef _ ->
     let error = str "This reference is not a constructor." in
-    user_err ~loc "find_constructor" error
+    user_err ~loc ~hdr:"find_constructor" error
   in
   cstr, match add_params with
     | Some nb_args ->
@@ -1085,7 +1085,7 @@ let sort_fields ~complete loc fields completer =
         let record =
           try Recordops.find_projection first_field_glob_ref
           with Not_found ->
-            user_err ~loc:(loc_of_reference first_field_ref) "intern"
+            user_err ~loc:(loc_of_reference first_field_ref) ~hdr:"intern"
                          (pr_reference first_field_ref ++ str": Not a projection")
         in
         (* the number of parameters *)
@@ -1114,7 +1114,7 @@ let sort_fields ~complete loc fields completer =
                            by a let-in in the record declaration
                            (its value is fixed from other fields). *)
                        if first_field && not regular && complete then
-                         user_err ~loc "" (str "No local fields allowed in a record construction.")
+                         user_err ~loc  (str "No local fields allowed in a record construction.")
                        else if first_field then
                          build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc
                        else if not regular && complete then
@@ -1127,7 +1127,7 @@ let sort_fields ~complete loc fields completer =
               | None :: projs ->
                  if complete then
                    (* we don't want anonymous fields *)
-                   user_err ~loc "" (str "This record contains anonymous fields.")
+                   user_err ~loc  (str "This record contains anonymous fields.")
                  else
                    (* anonymous arguments don't appear in proj_kinds *)
                    build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc
@@ -1141,13 +1141,13 @@ let sort_fields ~complete loc fields completer =
             | (field_ref, field_value) :: fields ->
                let field_glob_ref = try global_reference_of_reference field_ref
                with Not_found ->
-                 user_err ~loc:(loc_of_reference field_ref) "intern"
+                 user_err ~loc:(loc_of_reference field_ref) ~hdr:"intern"
                                (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
                let remaining_projs, (field_index, _) =
                  let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
-                   user_err ~loc ""
+                   user_err ~loc 
                      (str "This record contains fields of different records.")
                in
                index_fields fields remaining_projs ((field_index, field_value) :: acc)
@@ -1344,7 +1344,7 @@ let drop_notations_pattern looked_for =
 		 List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
 		 List.map (in_pat false scopes) args, [])
     | NList (x,y,iter,terminator,lassoc) ->
-      if not (List.is_empty args) then user_err ~loc ""
+      if not (List.is_empty args) then user_err ~loc 
         (strbrk "Application of arguments to a recursive notation not supported in patterns.");
       (try
          (* All elements of the list are in scopes (scopt,subscopes) *)
@@ -1464,10 +1464,10 @@ let extract_explicit_arg imps args =
 	  let id = match pos with
 	  | ExplByName id ->
 	      if not (exists_implicit_name id imps) then
-		user_err ~loc ""
+		user_err ~loc 
 		  (str "Wrong argument name: " ++ pr_id id ++ str ".");
 	      if Id.Map.mem id eargs then
-		user_err ~loc "" (str "Argument name " ++ pr_id id
+		user_err ~loc  (str "Argument name " ++ pr_id id
 		++ str " occurs more than once.");
 	      id
 	  | ExplByPos (p,_id) ->
@@ -1477,11 +1477,11 @@ let extract_explicit_arg imps args =
 		  if not (is_status_implicit imp) then failwith "imp";
 		  name_of_implicit imp
 		with Failure _ (* "nth" | "imp" *) ->
-		  user_err ~loc ""
+		  user_err ~loc 
 		    (str"Wrong argument position: " ++ int p ++ str ".")
 	      in
 	      if Id.Map.mem id eargs then
-		user_err ~loc "" (str"Argument at position " ++ int p ++
+		user_err ~loc  (str"Argument at position " ++ int p ++
 		  str " is mentioned more than once.");
 	      id in
 	  (Id.Map.add id (loc, a) eargs, rargs)
@@ -1636,7 +1636,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
        in
        begin
 	  match fields with
-	    | None -> user_err ~loc "intern" (str"No constructor inference.")
+	    | None -> user_err ~loc ~hdr:"intern" (str"No constructor inference.")
 	    | Some (n, constrname, args) ->
 		let pars = List.make n (CHole (loc, None, Misctypes.IntroAnonymous, None)) in
                 let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in
@@ -1859,7 +1859,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
       | (imp::impl', []) ->
 	  if not (Id.Map.is_empty eargs) then
 	    (let (id,(loc,_)) = Id.Map.choose eargs in
-	       user_err ~loc "" (str "Not enough non implicit \
+	       user_err ~loc  (str "Not enough non implicit \
 	    arguments to accept the argument bound to " ++
 		 pr_id id ++ str"."));
 	  []
@@ -1890,7 +1890,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     intern env c
   with
       InternalizationError (loc,e) ->
-	user_err ~loc "internalize"
+	user_err ~loc ~hdr:"internalize"
 	  (explain_internalization_error e)
 
 (**************************************************************************)
@@ -1930,7 +1930,7 @@ let intern_pattern globalenv patt =
     intern_cases_pattern globalenv (None,[]) empty_alias patt
   with
       InternalizationError (loc,e) ->
-	user_err ~loc "internalize" (explain_internalization_error e)
+	user_err ~loc ~hdr:"internalize" (explain_internalization_error e)
 
 
 (*********************************************************************)
@@ -2047,7 +2047,7 @@ let intern_context global_level env impl_env binders =
 	      tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
   (lenv.impls, List.map snd bl)
   with InternalizationError (loc,e) ->
-    user_err ~loc "internalize" (explain_internalization_error e)
+    user_err ~loc ~hdr:"internalize" (explain_internalization_error e)
 
 let interp_rawcontext_evars env evdref k bl =
   let (env, par, _, impls) =
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 19f76b972..9539980f0 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 ...*)
-      user_err "Coqlib.check_required_library"
+      user_err ~hdr:"Coqlib.check_required_library"
         (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
 
 (************************************************************************)
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8908e1f6f..28c92d95c 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -27,11 +27,11 @@ let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
 
 let declare_generalizable_ident table (loc,id) =
   if not (Id.equal id (root_of_id id)) then
-    user_err ~loc "declare_generalizable_ident"
+    user_err ~loc ~hdr:"declare_generalizable_ident"
     ((pr_id id ++ str
       " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
   if Id.Pred.mem id table then
-    user_err ~loc "declare_generalizable_ident"
+    user_err ~loc ~hdr:"declare_generalizable_ident"
 		((pr_id id++str" is already declared as a generalizable identifier"))
   else Id.Pred.add id table
 
@@ -78,7 +78,7 @@ let is_freevar ids env x =
 (* Auxiliary functions for the inference of implicitly quantified variables. *)
 
 let ungeneralizable loc id =
-  user_err ~loc "Generalization"
+  user_err ~loc ~hdr:"Generalization"
 	       (str "Unbound and ungeneralizable variable " ++ pr_id id)
 
 let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
@@ -203,7 +203,7 @@ let combine_params avoid fn applied needed =
             | Anonymous -> false
             in
 	    if not (List.exists is_id needed) then
-	      user_err ~loc "" (str "Wrong argument name: " ++ Nameops.pr_id id);
+	      user_err ~loc  (str "Wrong argument name: " ++ Nameops.pr_id id);
 	    true
 	| _ -> false) applied
   in
@@ -237,7 +237,7 @@ let combine_params avoid fn applied needed =
 	    aux (t' :: ids) avoid' app need
 
       | (x,_) :: _, [] ->
-	  user_err ~loc:(Constrexpr_ops.constr_loc x) "" (str "Typeclass does not expect more arguments")
+	  user_err ~loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
   in aux [] avoid applied needed
 
 let combine_params_freevar =
diff --git a/interp/notation.ml b/interp/notation.ml
index d50045546..c095435a5 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 =
-  user_err "Notation"
+  user_err ~hdr:"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.user_err "" (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
@@ -220,7 +220,7 @@ let remove_delimiters scope =
 let find_delimiters_scope loc key =
   try String.Map.find key !delimiters_map
   with Not_found ->
-    user_err ~loc "find_delimiters"
+    user_err ~loc ~hdr:"find_delimiters"
       (str "Unknown scope delimiting key " ++ str key ++ str ".")
 
 (* Uninterpretation tables *)
@@ -337,7 +337,7 @@ let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
 let check_required_module loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
   with Not_found ->
-    user_err ~loc "prim_token_interpreter"
+    user_err ~loc ~hdr:"prim_token_interpreter"
     (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
 
 (* Look if some notation or numeral printer in [scope] can be used in
@@ -458,7 +458,7 @@ let interp_prim_token_gen g loc p local_scopes =
   let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in
   try find_interpretation p_as_ntn (find_prim_token g loc p) scopes
   with Not_found ->
-    user_err ~loc "interp_prim_token"
+    user_err ~loc ~hdr:"interp_prim_token"
     ((match p with
       | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
@@ -483,7 +483,7 @@ let interp_notation loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
   try find_interpretation ntn (find_notation ntn) scopes
   with Not_found ->
-    user_err ~loc ""
+    user_err ~loc 
     (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
 
 let uninterp_notations c =
@@ -890,10 +890,10 @@ let global_reference_of_notation test (ntn,(sc,c,_)) =
   | _ -> None
 
 let error_ambiguous_notation loc _ntn =
-  user_err ~loc "" (str "Ambiguous notation.")
+  user_err ~loc  (str "Ambiguous notation.")
 
 let error_notation_not_reference loc ntn =
-  user_err ~loc ""
+  user_err ~loc 
    (str "Unable to interpret " ++ quote (str ntn) ++
     str " as a reference.")
 
@@ -1017,7 +1017,7 @@ let add_notation_extra_printing_rule ntn k v =
       let p, pp, gr = String.Map.find ntn !notation_rules in
       String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
   with Not_found ->
-    user_err "add_notation_extra_printing_rule"
+    user_err ~hdr:"add_notation_extra_printing_rule"
       (str "No such Notation.")
 
 (**********************************************************************)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d565f01ba..048cd5769 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -233,7 +233,7 @@ let split_at_recursive_part c =
 let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1)
 
 let check_is_hole id = function GHole _ -> () | t ->
-  user_err ~loc:(loc_of_glob_constr t) ""
+  user_err ~loc:(loc_of_glob_constr t)
    (strbrk "In recursive notation with binders, " ++ pr_id id ++
     strbrk " is expected to come without type.")
 
@@ -283,7 +283,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
 	let loc1 = loc_of_glob_constr iterator in
 	let loc2 = loc_of_glob_constr (Option.get !terminator) in
 	(* Here, we would need a loc made of several parts ... *)
-	user_err ~loc:(subtract_loc loc1 loc2) ""
+	user_err ~loc:(subtract_loc loc1 loc2)
           (str "Both ends of the recursive pattern are the same.")
     | Some (x,y,Some lassoc) ->
         let newfound,x,y,lassoc =
@@ -324,7 +324,7 @@ let notation_constr_and_vars_of_glob_constr a =
     | GApp (_,GVar (loc,f),[c]) when Id.equal f ldots_var ->
 	(* Fall on the second part of the recursive pattern w/o having
 	   found the first part *)
-	user_err ~loc ""
+	user_err ~loc 
 	(str "Cannot find where the recursive pattern starts.")
     | c ->
 	aux' c
@@ -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
-      user_err "" (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
-      user_err "" (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/reserve.ml b/interp/reserve.ml
index 31425fb98..a4d4f4027 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -86,12 +86,12 @@ let in_reserved : Id.t * notation_constr -> obj =
 
 let declare_reserved_type_binding (loc,id) t =
   if not (Id.equal id (root_of_id id)) then
-    user_err ~loc "declare_reserved_type"
+    user_err ~loc ~hdr:"declare_reserved_type"
       ((pr_id id ++ str
       " is not reservable: it must have no trailing digits, quote, or _"));
   begin try
     let _ = Id.Map.find id !reserve_table in
-    user_err ~loc "declare_reserved_type"
+    user_err ~loc ~hdr:"declare_reserved_type"
     ((pr_id id++str" is already bound to a type"))
   with Not_found -> () end;
   add_anonymous_leaf (in_reserved (id,t))
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 08425129b..178c1c1f9 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -46,7 +46,7 @@ let locate_global_with_alias ?(head=false) (loc,qid) =
     if head then global_of_extended_global_head ref
     else global_of_extended_global ref
   with Not_found ->
-    user_err ~loc "" (pr_qualid qid ++
+    user_err ~loc  (pr_qualid qid ++
       str " is bound to a notation that does not denote a reference.")
 
 let global_inductive_with_alias r =
@@ -54,7 +54,7 @@ let global_inductive_with_alias r =
   try match locate_global_with_alias lqid with
   | IndRef ind -> ind
   | ref ->
-      user_err ~loc:(loc_of_reference r) "global_inductive"
+      user_err ~loc:(loc_of_reference r) ~hdr:"global_inductive"
         (pr_reference r ++ spc () ++ str "is not an inductive type.")
   with Not_found -> Nametab.error_global_not_found ~loc qid
 
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 1e0964dd2..8135cd4dd 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
-    user_err "cache_syntax_constant"
+    user_err ~hdr:"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/interp/topconstr.ml b/interp/topconstr.ml
index ed44e66ff..0f894019b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -33,7 +33,7 @@ let _ = Goptions.declare_bool_option {
 (* Miscellaneous *)
 
 let error_invalid_pattern_notation ?loc =
-  user_err ?loc "" (str "Invalid notation for pattern.")
+  user_err ?loc  (str "Invalid notation for pattern.")
 
 (**********************************************************************)
 (* Functions on constr_expr *)
@@ -175,7 +175,7 @@ let split_at_annot bl na =
 	| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
         | LocalPattern _ :: rest -> assert false
 	| [] ->
-            user_err ~loc ""
+            user_err ~loc 
 			 (str "No parameter named " ++ Nameops.pr_id id ++ str".")
       in aux [] bl
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 9172fdbf0..c677a0f30 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.user_err "compile" else
+    let fn = if fail_on_error then CErrors.user_err ?loc:None ~hdr:"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 e2ee913a3..4a6b15653 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.user_err "export" (CErrors.iprint e)
+      CErrors.user_err ~hdr:"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.user_err "Safe_typing.import"
+    CErrors.user_err ~hdr:"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 340730558..08f888868 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
-      | _   -> user_err "to_lambda" (mt ())
+      | _   -> user_err ~hdr:"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
-      | _   -> user_err "to_prod" (mt ())
+      | _   -> user_err ~hdr:"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 94a05ef67..5b5739821 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
-      user_err "" (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 830a9e3ce..38ed3f5ba 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -33,12 +33,12 @@ let is_anomaly = function
 | Anomaly _ -> true
 | _ -> false
 
-exception UserError of string * std_ppcmds (* User errors *)
+exception UserError of string option * std_ppcmds (* User errors *)
 
 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 user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm))
+let error            string = user_err (str string)
 
 let invalid_arg ?loc s   = Loc.raise ?loc (Invalid_argument s)
 
@@ -112,7 +112,7 @@ let iprint_no_report (e, info) =
 
 let _ = register_handler begin function
   | UserError(s, pps) ->
-    hov 0 (str "Error: " ++ where (Some s) ++ pps)
+    hov 0 (str "Error: " ++ where s ++ pps)
   | _ -> raise Unhandled
 end
 
diff --git a/lib/cErrors.mli b/lib/cErrors.mli
index ad17be393..5cffc725d 100644
--- a/lib/cErrors.mli
+++ b/lib/cErrors.mli
@@ -33,11 +33,13 @@ val is_anomaly : exn -> bool
     This is mostly provided for compatibility. Please avoid doing specific
     tricks with anomalies thanks to it. See rather [noncritical] below. *)
 
-exception UserError of string * std_ppcmds
+exception UserError of string option * std_ppcmds
+(** Main error signaling exception. It carries a header plus a pretty printing
+    doc *)
 
-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 user_err : ?loc:Loc.t -> ?hdr:string -> std_ppcmds -> 'a
+(** Main error raising primitive. [user_err ?loc ?hdr pp] signals an
+    error [pp] with optional header and location [hdr] [loc] *)
 
 val error : string -> 'a
 (** [error s] just calls [user_error "_" (str s)] *)
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index f36c7ad80..18b26254d 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -45,7 +45,7 @@ let create ~name ~category ?(default=Enabled) pp =
            | Disabled -> ()
            | AsError ->
               let loc = Option.default !current_loc loc in
-              CErrors.user_err ~loc "_" (pp x)
+              CErrors.user_err ~loc (pp x)
            | Enabled ->
               let msg =
                 pp x ++ spc () ++ str "[" ++ str name ++ str "," ++
diff --git a/lib/system.ml b/lib/system.ml
index 916c08795..0f610b8d5 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.user_err "System.find_file_in_path"
+      CErrors.user_err ~hdr:"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.user_err "System.find_file_in_path"
+      CErrors.user_err ~hdr:"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.user_err "System.open" (str "Can't open " ++ str name)
+    CErrors.user_err ~hdr:"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.user_err "System" (str file ++ str ": " ++ str s ++ str ". Try to rebuild it.")
+  CErrors.user_err ~hdr:"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.user_err "System.extern_state" (str "System error: " ++ str s)
+    CErrors.user_err ~hdr:"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.user_err "System.intern_state" (str "System error: " ++ str s)
+    CErrors.user_err ~hdr:"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.user_err "with_magic_number_check"
+    CErrors.user_err ~hdr:"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/declare.ml b/library/declare.ml
index f8c3cddc4..cc8415cf4 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -462,7 +462,7 @@ let do_universe poly l =
   let in_section = Lib.sections_are_opened () in
   let () =
     if poly && not in_section then
-      user_err "Constraint"
+      user_err ~hdr:"Constraint"
                    (str"Cannot declare polymorphic universes outside sections")
   in
   let l =
@@ -496,19 +496,19 @@ let do_constraint poly l =
     fun (loc, id) ->
     try Idmap.find id names
     with Not_found ->
-      user_err ~loc "Constraint" (str "Undeclared universe " ++ pr_id id)
+      user_err ~loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id)
   in
   let in_section = Lib.sections_are_opened () in
   let () =
     if poly && not in_section then
-      user_err "Constraint"
+      user_err ~hdr:"Constraint"
                     (str"Cannot declare polymorphic constraints outside sections")
   in
   let check_poly loc p loc' p' =
     if poly then ()
     else if p || p' then
       let loc = if p then loc else loc' in
-      user_err ~loc "Constraint"
+      user_err ~loc ~hdr:"Constraint"
                     (str "Cannot declare a global constraint on " ++
                     str "a polymorphic universe, use "
                     ++ str "Polymorphic Constraint instead")
diff --git a/library/declaremods.ml b/library/declaremods.ml
index f388bc8b5..3a263b1e1 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 ->
-        user_err "consistency_checks"
+        user_err ~hdr:"consistency_checks"
           (pr_dirpath dir ++ str " should already exist!")
     in
     assert (eq_global_dir_reference globref dirinfo)
   else
     if Nametab.exists_dir dir then
-      user_err "consistency_checks"
+      user_err ~hdr:"consistency_checks"
         (pr_dirpath dir ++ str " already exists")
 
 let compute_visibility exists i =
diff --git a/library/goptions.ml b/library/goptions.ml
index b98cdac6a..db8933d28 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 =
-  user_err "Goptions" (str (nickname key) ++ str ": no table or option of this type")
+  user_err ~hdr:"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 f8990986c..c9d4afc79 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
-	  user_err ""
+	  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
-	  user_err ""
+	  user_err 
             (str "Bad implicit argument number: " ++ int i ++ str ".")
 	else
-	  user_err ""
+	  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
-    user_err "" (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 9d356bca8..376643ebb 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,_,_,_)) :: _ ->
-      user_err "Lib.classify_segment"
+      user_err ~hdr:"Lib.classify_segment"
         (str "there are still opened " ++ str (module_kind ty) ++ str "s")
     | (_,FrozenState _) :: stk -> clean acc stk
   in
@@ -267,7 +267,7 @@ let start_mod is_type export id mp fs =
     else Nametab.exists_module dir
   in
   if exists then
-    user_err "open_module" (pr_id id ++ str " already exists");
+    user_err ~hdr:"open_module" (pr_id id ++ str " already exists");
   add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs));
   path_prefix := prefix;
   prefix
@@ -277,7 +277,7 @@ let start_modtype = start_mod true None
 
 let error_still_opened string oname =
   let id = basename (fst oname) in
-  user_err ""
+  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,_,_,_) ->
-	user_err "Lib.end_compilation_checks"
+	user_err ~hdr:"Lib.end_compilation_checks"
           (str "There are some open " ++ str (module_kind ty) ++ str "s.")
       | _ -> assert false
     with Not_found -> ()
@@ -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
-      user_err "Lib.find_opening_node"
+      user_err ~hdr:"Lib.find_opening_node"
         (str "Last block to end has name " ++ pr_id id' ++ str ".");
     entry
   with Not_found -> error "There is nothing to end."
@@ -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
-    user_err "open_section" (pr_id id ++ str " already exists.");
+    user_err ~hdr:"open_section" (pr_id id ++ str " already exists.");
   let fs = Summary.freeze_summaries ~marshallable:`No in
   add_entry (make_oname id) (OpenedSection (prefix, fs));
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
diff --git a/library/library.ml b/library/library.ml
index 8d3916a97..c3d0485d3 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 ->
-    user_err "Library.find_library"
+    user_err ~hdr:"Library.find_library"
       (str "Unknown library " ++ pr_dirpath dir)
 
 let register_library_filename dir f =
@@ -329,12 +329,12 @@ let locate_qualified_library ?root ?(warn = true) qid =
 
 let error_unmapped_dir qid =
   let prefix, _ = repr_qualid qid in
-  user_err "load_absolute_library_from"
+  user_err ~hdr:"load_absolute_library_from"
     (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++
      str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ())
 
 let error_lib_not_found qid =
-  user_err "load_absolute_library_from"
+  user_err ~hdr:"load_absolute_library_from"
     (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath")
 
 let try_locate_absolute_library dir =
@@ -378,7 +378,7 @@ let access_table what tables dp i =
       let t =
         try fetch_delayed f
         with Faulty f ->
-          user_err "Library.access_table"
+          user_err ~hdr:"Library.access_table"
             (str "The file " ++ str f ++ str " (bound to " ++ str dir_path ++
              str ") is inaccessible or corrupted,\ncannot load some " ++
              str what ++ str " in it.\n")
@@ -463,7 +463,7 @@ let rec intern_library (needed, contents) (dir, f) from =
   let f = match f with Some f -> f | None -> try_locate_absolute_library dir in
   let m = intern_from_file f in
   if not (DirPath.equal dir m.library_name) then
-    user_err "load_physical_library"
+    user_err ~hdr:"load_physical_library"
       (str "The file " ++ str f ++ str " contains library" ++ spc () ++
        pr_dirpath m.library_name ++ spc () ++ str "and not library" ++
        spc() ++ pr_dirpath dir);
@@ -477,7 +477,7 @@ and intern_library_deps libs dir m from =
 and intern_mandatory_library caller from libs (dir,d) =
   let digest, libs = intern_library libs (dir, None) from in
   if not (Safe_typing.digest_match ~actual:digest ~required:d) then
-    user_err "" (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) =
@@ -572,7 +572,7 @@ let require_library_from_dirpath modrefl export =
 let safe_locate_module (loc,qid) =
   try Nametab.locate_module qid
   with Not_found ->
-    user_err ~loc "import_library"
+    user_err ~loc ~hdr:"import_library"
       (pr_qualid qid ++ str " is not a module")
 
 let import_module export modl =
@@ -597,7 +597,7 @@ let import_module export modl =
             flush acc;
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
-              user_err ~loc "import_library"
+              user_err ~loc ~hdr:"import_library"
                 (pr_qualid dir ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
@@ -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
-    user_err ""
+    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 = user_err "" (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 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");
+  if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
+  if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
+  if s3 = None then user_err ~hdr:"restart" (str"not a .vio file");
+  if pi3 (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
   longf, s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5
 
 (************************************************************************)
@@ -677,7 +677,7 @@ let current_deps () =
 let current_reexports () = !libraries_exports_list
 
 let error_recursively_dependent_library dir =
-  user_err ""
+  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.user_err "library"
+    if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library"
       Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
     opaque_table;
   let sd = {
diff --git a/library/nametab.ml b/library/nametab.ml
index 989dcf3f3..b76048e89 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -453,7 +453,7 @@ let global r =
   try match locate_extended qid with
     | TrueGlobal ref -> ref
     | SynDef _ ->
-        user_err ~loc "global"
+        user_err ~loc ~hdr:"global"
           (str "Unexpected reference to a notation: " ++
            pr_qualid qid)
   with Not_found ->
@@ -532,7 +532,7 @@ let global_inductive r =
   match global r with
   | IndRef ind -> ind
   | ref ->
-      user_err ~loc:(loc_of_reference r) "global_inductive"
+      user_err ~loc:(loc_of_reference r) ~hdr:"global_inductive"
         (pr_reference r ++ spc () ++ str "is not an inductive type")
 
 
diff --git a/library/universes.ml b/library/universes.ml
index 04b39937e..32eb35386 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.user_err "Universes"
+	CErrors.user_err ~hdr:"Universes"
 	  (str "Polymorphic constant expected " ++ int len2 ++ 
 	     str" levels but was given " ++ int len1)
       else ()
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index 85f1a0225..c67af33e2 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -36,7 +36,7 @@ let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c
 let reference_to_id = function
   | Libnames.Ident (loc, id) -> (loc, id)
   | Libnames.Qualid (loc,_) ->
-      CErrors.user_err ~loc ""
+      CErrors.user_err ~loc 
        (str "This expression should be a simple identifier.")
 
 let tactic_mode = Gram.entry_create "vernac:tactic_command"
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index e0583370a..18f67cad4 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 
-	     user_err "rewrite"
+	     user_err ~hdr:"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 ->
-	 user_err "" (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/tacentries.ml b/ltac/tacentries.ml
index 1b7430c3f..2fed0e14f 100644
--- a/ltac/tacentries.ml
+++ b/ltac/tacentries.ml
@@ -429,7 +429,7 @@ let register_ltac local tacl =
         let kn = Lib.make_kn id in
         let id_pp = pr_id id in
         let () = if is_defined_tac kn then
-          CErrors.user_err ~loc ""
+          CErrors.user_err ~loc 
             (str "There is already an Ltac named " ++ id_pp ++ str".")
         in
         let is_shadowed =
@@ -446,7 +446,7 @@ let register_ltac local tacl =
         let kn =
           try Nametab.locate_tactic (snd (qualid_of_reference ident))
           with Not_found ->
-            CErrors.user_err ~loc ""
+            CErrors.user_err ~loc 
                        (str "There is no Ltac named " ++ pr_reference ident ++ str ".")
         in
         UpdateTac kn, body
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml
index 5808feeba..e3c2b4ad5 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.user_err ""
+    CErrors.user_err 
       (str "The tactic " ++ pr_tacname s ++ str " is not installed.")
 
 (***************************************************************************)
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index a1d34b53f..cd791398d 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -33,7 +33,7 @@ open Locus
 let dloc = Loc.ghost
 
 let error_tactic_expected ?loc =
-  user_err ?loc "" (str "Tactic expected.")
+  user_err ?loc  (str "Tactic expected.")
 
 (** Generic arguments *)
 
@@ -461,7 +461,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
 let extract_let_names lrc =
   let fold accu ((loc, name), _) =
     if Id.Set.mem name accu then user_err ~loc
-      "glob_tactic" (str "This variable is bound several times.")
+      ~hdr:"glob_tactic" (str "This variable is bound several times.")
     else Id.Set.add name accu
   in
   List.fold_left fold Id.Set.empty lrc
@@ -748,7 +748,7 @@ let print_ltac id =
     ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
  with
   Not_found ->
-   user_err "print_ltac"
+   user_err ~hdr:"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 b1f554eaa..7d447b236 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
-    user_err "" (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
@@ -315,7 +315,7 @@ let append_trace trace v =
 (* Dynamically check that an argument is a tactic *)
 let coerce_to_tactic loc id v =
   let v = Value.normalize v in
-  let fail () = user_err ~loc ""
+  let fail () = user_err ~loc 
     (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
   in
   let v = Value.normalize v in
@@ -371,7 +371,7 @@ let debugging_exception_step ist signal_anomaly e pp =
     pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
 
 let error_ltac_variable loc id env v s =
-   user_err ~loc "" (str "Ltac variable " ++ pr_id id ++
+   user_err ~loc  (str "Ltac variable " ++ pr_id id ++
    strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
    strbrk "which cannot be coerced to " ++ str s ++ str".")
 
@@ -404,7 +404,7 @@ let interp_intro_pattern_naming_var loc ist env sigma id =
 let interp_int ist locid =
   try try_interp_ltac_var coerce_to_int ist None locid
   with Not_found ->
-    user_err ~loc:(fst locid) "interp_int"
+    user_err ~loc:(fst locid) ~hdr:"interp_int"
      (str "Unbound variable "  ++ pr_id (snd locid) ++ str".")
 
 let interp_int_or_var ist = function
@@ -795,7 +795,7 @@ let interp_may_eval f ist env sigma = function
 	!evdref , c
       with
 	| Not_found ->
-	    user_err ~loc "interp_may_eval"
+	    user_err ~loc ~hdr:"interp_may_eval"
 	    (str "Unbound context identifier" ++ pr_id s ++ str"."))
   | ConstrTypeOf c ->
       let (sigma,c_interp) = f ist env sigma c in
@@ -1032,7 +1032,7 @@ let interp_destruction_arg ist gl arg =
       }
   | keep,ElimOnAnonHyp n as x -> x
   | keep,ElimOnIdent (loc,id) ->
-      let error () = user_err ~loc ""
+      let error () = user_err ~loc 
        (strbrk "Cannot coerce " ++ pr_id id ++
         strbrk " neither to a quantified hypothesis nor to a term.")
       in
@@ -1043,7 +1043,7 @@ let interp_destruction_arg ist gl arg =
           (keep, ElimOnConstr { delayed = begin fun env sigma ->
           try Sigma.here (constr_of_id env id', NoBindings) sigma
           with Not_found ->
-            user_err ~loc  "interp_destruction_arg" (
+            user_err ~loc  ~hdr:"interp_destruction_arg" (
             pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
           end })
       in
@@ -1111,7 +1111,7 @@ let read_pattern lfun ist env sigma = function
 (* Reads the hypotheses of a Match Context rule *)
 let cons_and_check_name id l =
   if Id.List.mem id l then
-    user_err "read_match_goal_hyps" (
+    user_err ~hdr:"read_match_goal_hyps" (
       str "Hypothesis pattern-matching variable " ++ pr_id id ++
       str " used twice in the same pattern.")
   else id::l
@@ -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 *) ->
-              user_err "" (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 7d3cb7e49..0dbe08231 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
-  user_err ""
+  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/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 92a59be43..7021e5270 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -56,7 +56,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) =
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = Option.map (fun (aloc,_) ->
     CErrors.user_err ~loc:aloc
-      "Constr:mk_cofixb"
+      ~hdr:"Constr:mk_cofixb"
       (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in
   let ty = match tyc with
       Some ty -> ty
@@ -381,12 +381,12 @@ GEXTEND Gram
         (match p with
 	  | CPatAtom (_, Some r) -> CPatCstr (!@loc, r, None, lp)
 	  | CPatCstr (_, r, None, l2) -> CErrors.user_err
-              ~loc:(cases_pattern_expr_loc p) "compound_pattern"
+              ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
               (Pp.str "Nested applications not supported.")
 	  | CPatCstr (_, r, l1, l2) -> CPatCstr (!@loc, r, l1 , l2@lp)
 	  | CPatNotation (_, n, s, l) -> CPatNotation (!@loc, n , s, l@lp)
           | _ -> CErrors.user_err
-              ~loc:(cases_pattern_expr_loc p) "compound_pattern"
+              ~loc:(cases_pattern_expr_loc p) ~hdr:"compound_pattern"
               (Pp.str "Such pattern cannot have arguments."))
       |"@"; r = Prim.reference; lp = LIST0 NEXT ->
         CPatCstr (!@loc, r, Some lp, []) ]
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index b447a5de5..820514b08 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -28,7 +28,7 @@ let my_int_of_string loc s =
     if n > 1024 * 2048 then raise Exit;
     n
   with Failure _ | Exit ->
-    CErrors.user_err ~loc "" (Pp.str "Cannot support a so large number.")
+    CErrors.user_err ~loc  (Pp.str "Cannot support a so large number.")
 
 GEXTEND Gram
   GLOBAL:
@@ -93,7 +93,7 @@ GEXTEND Gram
   ;
   ne_string:
     [ [ s = STRING ->
-        if s="" then CErrors.user_err ~loc:(!@loc) "" (Pp.str"Empty string."); s
+        if s="" then CErrors.user_err ~loc:(!@loc) (Pp.str"Empty string."); s
     ] ]
   ;
   ne_lstring:
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 2cc2b01c0..3c2c45c72 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -136,7 +136,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
 let mk_cofix_tac (loc,id,bl,ann,ty) =
   let _ = Option.map (fun (aloc,_) ->
     user_err ~loc:aloc
-      "Constr:mk_cofix_tac"
+      ~hdr:"Constr:mk_cofix_tac"
       (Pp.str"Annotation forbidden in cofix expression.")) ann in
   (id,CProdN(loc,bl,ty))
 
@@ -192,7 +192,7 @@ let merge_occurrences loc cl = function
   | None ->
       if Locusops.clause_with_generic_occurrences cl then (None, cl)
       else
-	user_err ~loc "" (str "Found an \"at\" clause without \"with\" clause.")
+	user_err ~loc  (str "Found an \"at\" clause without \"with\" clause.")
   | Some (occs, p) ->
     let ans = match occs with
     | AllOccurrences -> cl
@@ -204,9 +204,9 @@ let merge_occurrences loc cl = function
         { cl with onhyps = Some [(occs, id), l] }
       | _ ->
         if Locusops.clause_with_generic_occurrences cl then
-          user_err ~loc "" (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
+          user_err ~loc  (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.")
         else
-          user_err ~loc "" (str "Cannot use clause \"at\" twice.")
+          user_err ~loc  (str "Cannot use clause \"at\" twice.")
       end
     in
     (Some p, ans)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c09693b36..7cb897cf7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -115,7 +115,7 @@ GEXTEND Gram
                     | Some (SelectNth g) -> c (Some g)
                     | None -> c None
                     | _ ->
-                        VernacError (UserError ("",str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
+                        VernacError (UserError (None,str"Typing and evaluation commands, cannot be used with the \"all:\" selector."))
                   end ] ]
   ;
   located_vernac:
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 6ed678176..71e2180a5 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 =
-  user_err  "Congruence" (Pp.str "congruence failed.")
+  user_err ~hdr:"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 9ed5c61e2..f68c01b18 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -91,7 +91,7 @@ let rec add_vars_of_simple_pattern globs = function
 	(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
   | CPatOr (loc, _)->
       Loc.raise ~loc
-	(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
+	(UserError (Some "simple_pattern",str "\"(_ | _)\" is not allowed here"))
   | CPatDelimiters (_,_,p) ->
       add_vars_of_simple_pattern globs p
   | CPatCstr (_,_,pl1,pl2) ->
@@ -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
-	user_err "suppose it is" 
+	user_err ~hdr:"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
-	  user_err "suppose it is"
+	  user_err ~hdr:"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 9510ba384..4649b1005 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, _) ->
-      user_err "" (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
-    user_err "thesis_for"
+    user_err ~hdr:"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
-    user_err "thesis_for"
+    user_err ~hdr:"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 3c26c4710..5e7d810c9 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 = user_err "Extraction" s
+let err s = user_err ~hdr:"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 f4daa0323..718448fc1 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 ->
-                user_err "FunInd.build_scheme"
+                user_err ~hdr:"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 ->
-      user_err "FunInd.build_case_scheme"
+      user_err ~hdr:"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 9902b0128..56ba0cba9 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 ->
-	    user_err "" (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 ->
-	      user_err "" (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
@@ -1198,7 +1198,7 @@ let rec compute_cst_params relnames params = function
   | GSort _ -> params
   | GHole _ -> params
   | GIf _ | GRec _ | GCast _ ->
-      raise (UserError("compute_cst_params", str "Not handled case"))
+      raise (UserError(Some "compute_cst_params", str "Not handled case"))
 and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 01e5ef7fb..4e561fc7e 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -406,7 +406,7 @@ let is_free_in id =
 
     | GIf(_,cond,_,br1,br2) ->
 	is_free_in cond || is_free_in br1 || is_free_in br2
-    | GRec _ -> raise (UserError("",str "Not handled GRec"))
+    | GRec _ -> raise (UserError(None,str "Not handled GRec"))
     | GSort _ -> false
     | GHole _ -> false
     | GCast (_,b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
@@ -502,7 +502,7 @@ let replace_var_by_term x_id term =
 	      replace_var_by_pattern lhs,
 	      replace_var_by_pattern rhs
 	     )
-      | GRec _ -> raise (UserError("",str "Not handled GRec"))
+      | GRec _ -> raise (UserError(None,str "Not handled GRec"))
       | GSort _ -> rt
       | GHole _ -> rt
       | GCast(loc,b,c) ->
@@ -655,7 +655,7 @@ let zeta_normalize =
 	      zeta_normalize_term lhs,
 	      zeta_normalize_term rhs
 	     )
-      | GRec _ -> raise (UserError("",str "Not handled GRec"))
+      | GRec _ -> raise (UserError(None,str "Not handled GRec"))
       | GSort _ -> rt
       | GHole _ -> rt
       | GCast(loc,b,c) ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 943ebc9fc..61e31277f 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 ->
-		    user_err "" (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,11 +70,11 @@ 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 ! *)
-		    user_err "" (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')
-	   | _ -> raise (UserError("",str "functional induction must be used with a function" ))
+	   | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
 	 end
       | Some ((princ,binding)) ->
 	 princ,binding,Tacmach.pf_unsafe_type_of g princ,g
@@ -175,7 +175,7 @@ let build_newrecursive l =
        match body_opt with 
 	 | Some body -> 
 	     (fixna,bll,ar,body)
-	 | None -> user_err "Function" (str "Body of Function must be given")
+	 | None -> user_err ~hdr:"Function" (str "Body of Function must be given")
     ) l
   in
   build_newrecursive l'
@@ -321,7 +321,7 @@ let error_error names e =
   in
   match e with
     | Building_graph e ->
-	user_err ""
+	user_err 
 	  (str "Cannot define graph(s) for " ++
 	     h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
 	     e_explain e)
@@ -391,7 +391,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
   match fixpoint_exprl with
     | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
-      let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in 
+      let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
       Command.do_definition
 	fname
 	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
@@ -630,7 +630,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	      | _ -> assert false
 	  in 
 	  let fixpoint_exprl = [fixpoint_expr] in 
-	  let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in 
+	  let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
 	  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	  let using_lemmas = [] in 
 	  let pre_hook pconstants =
@@ -656,7 +656,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
 	  let fixpoint_exprl = [fixpoint_expr] in 
 	  let recdefs,rec_impls = build_newrecursive fixpoint_exprl in
 	  let using_lemmas = [] in
-	  let body = match body with | Some body -> body | None -> user_err "Function" (str "Body of Function must be given") in 
+	  let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
 	  let pre_hook pconstants =
 	    generate_principle
 	      (ref (Evd.from_env (Global.env ())))
@@ -834,9 +834,9 @@ let make_graph (f_ref:global_reference) =
       | ConstRef c ->
 	  begin try c,Global.lookup_constant c
 	  with Not_found ->
-	    raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
+	    raise (UserError (None,str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) )
 	  end
-      | _ -> raise (UserError ("", str "Not a function reference") )
+      | _ -> raise (UserError (None, str "Not a function reference") )
   in
   (match Global.body_of_constant_body c_body with
      | None -> error "Cannot build a graph over an axiom !"
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a1c94f8cb..a45effb16 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -49,7 +49,7 @@ let locate_constant ref =
 
 let locate_with_msg msg f x =
   try f x
-  with Not_found -> raise (CErrors.UserError("", msg))
+  with Not_found -> raise (CErrors.UserError(None, msg))
 
 
 let filter_map filter f =
@@ -73,7 +73,7 @@ let chop_rlambda_n  =
 	  | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b
 	  | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b
 	  | _ ->
-	      raise (CErrors.UserError("chop_rlambda_n",
+	      raise (CErrors.UserError(Some "chop_rlambda_n",
 				    str "chop_rlambda_n: Not enough Lambdas"))
   in
   chop_lambda_n []
@@ -85,7 +85,7 @@ let chop_rprod_n  =
       else
 	match rt with
 	  | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
-	  | _ -> raise (CErrors.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products"))
+	  | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
   chop_prod_n []
 
@@ -110,7 +110,7 @@ let const_of_id id =
   in
   try Constrintern.locate_reference princ_ref
   with Not_found ->
-    CErrors.user_err "IndFun.const_of_id"
+    CErrors.user_err ~hdr:"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 ee1232013..e86231ba9 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -998,7 +998,7 @@ let invfun qhyp f  =
   let f =
     match f with
       | ConstRef f -> f
-      | _ -> raise (CErrors.UserError("",str "Not a function"))
+      | _ -> raise (CErrors.UserError(None,str "Not a function"))
   in
   try
     let finfos = find_Function_infos f in
@@ -1043,19 +1043,19 @@ let invfun qhyp f g =
 			 functional_inversion kn hid  f2 f_correct g
 		       with
 			 | Failure "" ->
-			     user_err "" (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 user_err "" (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 user_err "" (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
-	       | _ -> user_err "" (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 0b93a909a..76c5afec6 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 ->
-      user_err "indfun" (Nameops.pr_id id ++ str " has no functional scheme")
+      user_err ~hdr:"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 7745e8498..19c6ec8f4 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 user_err "Recdef.check_not_nested"
+        then user_err ~hdr:"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) -> 
-    user_err "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
+    user_err ~hdr:"_" (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 ->
-	  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)
+	  user_err ~hdr:"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 ->
-	  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)
+	  user_err ~hdr:"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 _ ->  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)")
+	  | Case _ ->  user_err ~hdr:"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}
@@ -723,8 +723,8 @@ let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
 	 (List.map_i (fun i e -> observe_tac (str "do treat case") (treat_case f_is_present to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
 	 ))
     with 
-      | UserError("Refiner.thensn_tac3",_) 
-      | UserError("Refiner.tclFAIL_s",_) ->
+      | UserError(Some "Refiner.thensn_tac3",_) 
+      | UserError(Some "Refiner.tclFAIL_s",_) ->
 	(observe_tac (str "is computable " ++ Printer.pr_lconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
 	))
     g
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 9cfcb0fb7..367a13333 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 user_err "rtauto" (Pp.str "goal should be in Prop") in
+    then user_err ~hdr:"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 ->
-      user_err "rtauto" (Pp.str "rtauto couldn't find any proof") in
+      user_err ~hdr:"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 7450aa23e..a5e2211d8 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 ->
-    user_err"lookup_map"(str"map "++qs map++str"not found")
+    user_err ~hdr:"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
-            user_err "ring"
+            user_err ~hdr:"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 ->
-          user_err "ring"
+          user_err ~hdr:"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
-            user_err "field"
+            user_err ~hdr:"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 ->
-          user_err "field"
+          user_err ~hdr:"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 199c26363..5fb0bb664 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -61,8 +61,8 @@ DECLARE PLUGIN "ssrmatching_plugin"
 
 type loc = Loc.t
 let dummy_loc = Loc.ghost
-let errorstrm = CErrors.user_err "ssrmatching"
-let loc_error loc msg = CErrors.user_err ~loc msg (str msg)
+let errorstrm = CErrors.user_err ~hdr:"ssrmatching"
+let loc_error loc msg = CErrors.user_err ~loc ~hdr:msg (str msg)
 let ppnl = Feedback.msg_info
 
 (* 0 cost pp function. Active only if env variable SSRDEBUG is set *)
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index c6fe553c5..ed8cc6ab0 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -52,7 +52,7 @@ let interp_ascii_string dloc s =
       if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
       then int_of_string s
       else
-	user_err ~loc:dloc "interp_ascii_string"
+	user_err ~loc:dloc ~hdr:"interp_ascii_string"
 	 (str "Expects a single character or a three-digits ascii code.") in
   interp_ascii dloc p
 
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 6d62496ee..ab262fea7 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -47,7 +47,7 @@ let nat_of_int dloc n =
       mk_nat ref_O n
     end
   else
-      user_err "nat_of_int"
+      user_err ~hdr:"nat_of_int"
        (str "Cannot interpret a negative number as a number of type nat")
 
 (************************************************************************)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index ac28714f5..a25ddb062 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -100,7 +100,7 @@ let int31_of_pos_bigint dloc n =
   GApp (dloc, ref_construct, List.rev (args 31 n))
 
 let error_negative dloc =
-  CErrors.user_err ~loc:dloc "interp_int31" (Pp.str "int31 are only non-negative numbers.")
+  CErrors.user_err ~loc:dloc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
 
 let interp_int31 dloc n =
   if is_pos_or_zero n then
@@ -189,7 +189,7 @@ let bigN_of_pos_bigint dloc n =
   GApp (dloc, ref_constructor, args)
 
 let bigN_error_negative dloc =
-  CErrors.user_err ~loc:dloc "interp_bigN" (Pp.str "bigN are only non-negative numbers.")
+  CErrors.user_err ~loc:dloc ~hdr:"interp_bigN" (Pp.str "bigN are only non-negative numbers.")
 
 let interp_bigN dloc n =
   if is_pos_or_zero n then
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 851ea3b74..b7b5fb8a5 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -57,7 +57,7 @@ let pos_of_bignat dloc x =
   pos_of x
 
 let error_non_positive dloc =
-  user_err ~loc:dloc "interp_positive"
+  user_err ~loc:dloc ~hdr:"interp_positive"
    (str "Only strictly positive numbers in type \"positive\".")
 
 let interp_positive dloc n =
@@ -113,7 +113,7 @@ let n_of_binnat dloc pos_or_neg n =
     GRef (dloc, glob_N0, None)
 
 let error_negative dloc =
-  user_err ~loc:dloc "interp_N" (str "No negative numbers in type \"N\".")
+  user_err ~loc:dloc ~hdr:"interp_N" (str "No negative numbers in type \"N\".")
 
 let n_of_int dloc n =
   if is_pos_or_zero n then n_of_binnat dloc true n
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 18ad2ed3d..0e659aec9 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
-    | [] -> user_err "build_leaf" (msg_may_need_inversion())
+    | [] -> user_err ~hdr:"build_leaf" (msg_may_need_inversion())
     | eqn::_ ->
 	set_used_pattern eqn;
         eqn.rhs
@@ -1832,7 +1832,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 		       | None -> [LocalAssum (na, lift n typ)]
 		       | Some b -> [LocalDef (na, lift n b, lift n typ)])
 	    | Some (loc,_,_) ->
- 	    user_err ~loc ""
+ 	    user_err ~loc 
                 (str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = if dolift then lift_inductive_family n indf else indf in
@@ -1843,7 +1843,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
 	    match t with
 	      | Some (loc,ind',realnal) ->
 		  if not (eq_ind ind ind') then
-		    user_err ~loc "" (str "Wrong inductive type.");
+		    user_err ~loc  (str "Wrong inductive type.");
 		  if not (Int.equal nrealargs_ctxt (List.length realnal)) then
 		      anomaly (Pp.str "Ill-formed 'in' clause in cases");
 		  List.rev realnal
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 92a0ca988..30d100af9 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
-    user_err "try_add_coercion"
+    user_err ~hdr:"try_add_coercion"
       (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion.");
   ref
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ab9393915..cad5551c1 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -67,14 +67,14 @@ let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1
 let encode_bool r =
   let (x,lc) = encode_inductive r in
   if not (has_two_constructors lc) then
-    user_err ~loc:(loc_of_reference r) "encode_if"
+    user_err ~loc:(loc_of_reference r) ~hdr:"encode_if"
       (str "This type has not exactly two constructors.");
   x
 
 let encode_tuple r =
   let (x,lc) = encode_inductive r in
   if not (isomorphic_to_tuple lc) then
-    user_err ~loc:(loc_of_reference r) "encode_tuple"
+    user_err ~loc:(loc_of_reference r) ~hdr:"encode_tuple"
       (str "This type cannot be seen as a tuple type.");
   x
 
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index c7909a3c7..38b6075e5 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 =
-  user_err "" (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 0061d8ae9..9cf91a947 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
-    user_err ""(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 ->
-    user_err "default_elim"
+    user_err ~hdr:"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 cb69ab36f..29f57144a 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
-       user_err "make_case_or_project"
+       user_err ~hdr:"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 aa795106a..9dcb5d2a5 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -204,7 +204,7 @@ let error_instantiate_pattern id l =
   | [_] -> "is" 
   | _ -> "are"
   in
-  user_err "" (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.")
 
@@ -315,7 +315,7 @@ let rec subst_pattern subst pat =
 let mkPLambda na b = PLambda(na,PMeta None,b)
 let rev_it_mkPLambda = List.fold_right mkPLambda
 
-let err ?loc pp = user_err ?loc "pattern_of_glob_constr" pp
+let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp
 
 let warn_cast_in_pattern =
   CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
@@ -387,7 +387,7 @@ let rec pat_of_raw metas vars = function
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
         | (None | Some (GHole _)), _ -> PMeta None
 	| Some p, None ->
-            user_err ~loc "" (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
+            user_err ~loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
 	{ cip_style = sty;
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cdb39207e..3e65363d6 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -160,7 +160,7 @@ let search_guard loc env possible_indexes fixdefs =
 	    with TypeError _ -> ())
 	 (List.combinations possible_indexes);
        let errmsg = "Cannot guess decreasing argument of fix." in
-	 user_err ~loc "search_guard" (Pp.str errmsg)
+	 user_err ~loc ~hdr:"search_guard" (Pp.str errmsg)
      with Found indexes -> indexes)
 
 (* To force universe name declaration before use *)
@@ -211,7 +211,7 @@ let interp_universe_level_name evd (loc,s) =
 	with Not_found -> 
 	  if not (is_strict_universe_declarations ()) then
   	    new_univ_level_variable ~loc ~name:s univ_rigid evd
-	  else user_err ~loc "interp_universe_level_name"
+	  else user_err ~loc ~hdr:"interp_universe_level_name"
 			     (Pp.(str "Undeclared universe: " ++ str s))
 
 let interp_universe ?loc evd = function
@@ -373,9 +373,9 @@ let check_instance loc subst = function
   | [] -> ()
   | (id,_) :: _ ->
       if List.mem_assoc id subst then
-        user_err ~loc "" (pr_id id ++ str "appears more than once.")
+        user_err ~loc  (pr_id id ++ str "appears more than once.")
       else
-        user_err ~loc "" (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
+        user_err ~loc  (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
 
 (* used to enforce a name in Lambda when the type constraints itself
    is named, hence possibly dependent *)
@@ -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
-          user_err "" (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 ->
-    user_err "" (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 _ ->
-    user_err ""
+    user_err 
       (str "Cannot reinterpret " ++ quote (print_constr c) ++
        str " in the current environment.")
 
@@ -454,7 +454,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
 	(* and build a nice error message *)
       if Id.Map.mem id lvar.ltac_genargs then begin
         let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
-	user_err ~loc ""
+	user_err ~loc 
          (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \
           bound to a " ++ Geninterp.Val.pr typ ++ str ".")
       end;
@@ -486,7 +486,7 @@ let pretype_global loc rigid env evd gr us =
        let arr = Univ.Instance.to_array (Univ.UContext.instance ctx) in
        let len = Array.length arr in
        if len != List.length l then
-	 user_err ~loc "pretype"
+	 user_err ~loc ~hdr:"pretype"
 		       (str "Universe instance should have length " ++ int len)
        else
 	 let evd, l' = List.fold_left (fun (evd, univs) l -> 
@@ -494,7 +494,7 @@ let pretype_global loc rigid env evd gr us =
 	      (evd, l :: univs)) (evd, []) l
 	 in
 	 if List.exists (fun l -> Univ.Level.is_prop l) l' then
-	   user_err ~loc "pretype"
+	   user_err ~loc ~hdr:"pretype"
 		 (str "Universe instances cannot contain Prop, polymorphic" ++
 		   str " universe instances must be greater or equal to Set.");
 	 evd, Some (Univ.Instance.of_array (Array.of_list (List.rev l')))
@@ -566,7 +566,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
       let evk =
         try Evd.evar_key id !evdref
         with Not_found ->
-          user_err ~loc "" (str "Unknown existential variable.") in
+          user_err ~loc  (str "Unknown existential variable.") in
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
       let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
       let c = mkEvar (evk, args) in
@@ -848,11 +848,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
     in
     let cstrs = get_constructors env.ExtraEnv.env indf in
     if not (Int.equal (Array.length cstrs) 1) then
-      user_err ~loc "" (str "Destructing let is only for inductive types" ++
+      user_err ~loc  (str "Destructing let is only for inductive types" ++
 	str " with one constructor.");
     let cs = cstrs.(0) in
     if not (Int.equal (List.length nal) cs.cs_nargs) then
-      user_err ~loc:loc "" (str "Destructing let on this type expects " ++ 
+      user_err ~loc:loc (str "Destructing let on this type expects " ++ 
 	int cs.cs_nargs ++ str " variables.");
     let fsign, record = 
       match get_projections env.ExtraEnv.env indf with
@@ -937,7 +937,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  error_case_not_inductive ~loc:cloc env.ExtraEnv.env !evdref cj in
     let cstrs = get_constructors env.ExtraEnv.env indf in
       if not (Int.equal (Array.length cstrs) 2) then
-        user_err ~loc ""
+        user_err ~loc 
 		      (str "If is only for inductive types with two constructors.");
 
       let arsgn =
@@ -1022,7 +1022,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		else
 		  error_actual_type ~loc env.ExtraEnv.env !evdref cj tval 
                       (ConversionFailed (env.ExtraEnv.env,cty,tval))
-	      else user_err ~loc "" (str "Cannot check cast with vm: " ++
+	      else user_err ~loc  (str "Cannot check cast with vm: " ++
 		str "unresolved arguments remain.")
 	  | NATIVEcast ->
  	    let cj = pretype empty_tycon env evdref lvar c in
@@ -1059,7 +1059,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
         let t' = lookup_named id env |> get_type in
         if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found
       with Not_found ->
-        user_err ~loc "" (str "Cannot interpret " ++
+        user_err ~loc  (str "Cannot interpret " ++
           pr_existential_key !evdref evk ++
           str " in current context: no binding for " ++ pr_id id ++ str ".") in
     ((id,c)::subst, update) in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 945ef5daa..cda052b79 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 =
-  user_err "object_declare"
+  user_err ~hdr:"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/reductionops.ml b/pretyping/reductionops.ml
index 5484e70b6..ba1b4a10a 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1205,7 +1205,7 @@ let pb_equal = function
   | Reduction.CONV -> Reduction.CONV
 
 let report_anomaly _ =
-  let e = UserError ("", Pp.str "Conversion test raised an anomaly") in
+  let e = UserError (None, Pp.str "Conversion test raised an anomaly") in
   let e = CErrors.push e in
   iraise e
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 67819dc98..bb883b29f 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -38,7 +38,7 @@ exception Elimconst
 exception Redelimination
 
 let error_not_evaluable r =
-  user_err "error_not_evaluable"
+  user_err ~hdr:"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
-          user_err "" (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
-    user_err "" (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
-      user_err "" (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
-	    user_err "" (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)
-	    | _ -> user_err "" (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 =
-  user_err ""
+  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 5e3c3c259..bc009e50a 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
-      user_err "Unification.make_abstraction_core"
+      user_err ~hdr:"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
-          user_err "" (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 e2fefa5c8..ea89cd432 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -700,7 +700,7 @@ let read_sec_context r =
   let dir =
     try Nametab.locate_section qid
     with Not_found ->
-      user_err ~loc "read_sec_context" (str "Unknown section.") in
+      user_err ~loc ~hdr:"read_sec_context" (str "Unknown section.") in
   let rec get_cxt in_cxt = function
     | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest ->
         if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest
@@ -737,7 +737,7 @@ let print_any_name = function
     str |> Global.lookup_named |> set_id str |> print_named_decl
   with Not_found ->
     user_err
-      "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
+      ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
 let print_name = function
   | ByNotation (loc,ntn,sc) ->
@@ -831,7 +831,7 @@ let index_of_class cl =
   try
     fst (class_info cl)
   with Not_found ->
-    user_err "index_of_class"
+    user_err ~hdr:"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 ->
-      user_err "index_cl_of_id"
+      user_err ~hdr:"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 0ee13bb63..fad656223 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 ->
-        user_err "clenv_assign"
+        user_err ~hdr:"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 :: _ ->
-	user_err ""
+	user_err 
 	  (str "The variable " ++ pr_id s ++
 	   str " occurs more than once in binding list.");
     | AnonHyp n :: _ ->
-	user_err ""
+	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
-  user_err "Evd.meta_with_name"
+  user_err ~hdr:"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
     | _  ->
-        user_err "Evd.meta_with_name"
+        user_err ~hdr:"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 _) ->
-        user_err "" (str "No such binder.")
+        user_err  (str "No such binder.")
 
 let error_already_defined b =
   match b with
     | NamedHyp id ->
-        user_err ""
+        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 =
-  user_err ""
+  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
-  user_err "" (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
   | _ ->
-    user_err ""
+    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 ->
-    user_err "" (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/evar_refiner.ml b/proofs/evar_refiner.ml
index ce216e563..ff0df9179 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -54,7 +54,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
-      user_err ~loc ""
+      user_err ~loc 
                 (str "Instance is not well-typed in the environment of " ++
                  pr_existential_key sigma evk ++ str ".")
   in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 9f34f5cf6..3e77bef7e 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
-            user_err "reorder_context"
+            user_err ~hdr:"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
-    user_err "Logic.check_decl_position"
+    user_err ~hdr:"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
-	      user_err "move_hyp" (str "Cannot move " ++ pr_id (get_id declfrom) ++
+	      user_err ~hdr:"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 =
-  user_err "" (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
-	  user_err "Logic.convert_hyp"
+	  user_err ~hdr:"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
-	  user_err "Logic.convert_hyp"
+	  user_err ~hdr:"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
-	      user_err "Logic.prim_refiner"
+	      user_err ~hdr:"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 b86582def..86c2b7a57 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.user_err "" msg
+	                            CErrors.user_err  msg
         | _ -> assert false
 
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
@@ -228,7 +228,7 @@ let solve_by_implicit_tactic env sigma evk =
       when
 	Context.Named.equal (Environ.named_context_of_val evi.evar_hyps)
 	(Environ.named_context env) ->
-      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in
+      let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
       (try
         let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
         if Evarutil.has_undefined_evars sigma c then raise Exit;
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 2e5330b4b..16278b456 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.user_err "Focus" Pp.(str"No such goal (" ++ int i ++ str").")
+      CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
-      CErrors.user_err "Focus" Pp.(
+      CErrors.user_err ~hdr:"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 107a3a7e5..da0af3c62 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -203,7 +203,7 @@ let discard (loc,id) =
   discard_gen id;
   if Int.equal (List.length !pstates) n then
     CErrors.user_err ~loc
-      "Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
+      ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
   if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates
@@ -408,7 +408,7 @@ let return_proof ?(allow_partial=false) () =
   let evd =
     let error s =
       let prf = str " (in proof " ++ Id.print pid ++ str ")" in
-      raise (CErrors.UserError("last tactic before Qed",s ++ prf))
+      raise (CErrors.UserError(Some "last tactic before Qed",s ++ prf))
     in
     try Proof.return proof with
     | Proof.UnfinishedProof ->
@@ -519,7 +519,7 @@ module Bullet = struct
 	(function
 	| FailedBullet (b,sugg) ->
 	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
-	  CErrors.user_err "Focus" (prefix ++ suggest_on_error sugg)
+	  CErrors.user_err ~hdr:"Focus" (prefix ++ suggest_on_error sugg)
 	| _ -> raise CErrors.Unhandled)
 
 
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index cafd46849..41ad7d94e 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 _ ->
-            user_err "set_transparent_const"
+            user_err ~hdr:"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 user_err "Redexpr.declare_reduction"
+  then user_err ~hdr:"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 user_err "Redexpr.check_custom" (str "Reference to undefined reduction expression " ++ str s)
+      then user_err ~hdr:"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 user_err "Redexpr.decl_red_expr"
+  then user_err ~hdr:"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 ->
-	   user_err "Redexpr.reduction_of_red_expr"
+	   user_err ~hdr:"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 65a889882..3e59631b7 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 = user_err "Refiner.tclFAIL_s" (str s)
+let tclFAIL_s s gls = user_err ~hdr:"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 user_err "Refiner.thensn_tac" (str "Not enough subgoals.");
+  if ng<nf+nl then user_err ~hdr:"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 user_err "Refiner.WEAK_PROGRESS" (str"Failed to progress.")
+  else user_err ~hdr:"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 user_err "Refiner.PROGRESS" (str"Failed to progress.")
+  else user_err ~hdr:"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 user_err "Refiner.tclNOTSAMEGOAL"
+  then user_err ~hdr:"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 user_err "Refiner.tclDO"
+    if k < 0 then user_err ~hdr:"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/lemmas.ml b/stm/lemmas.ml
index 4552ba8c6..b08296fb9 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -222,7 +222,7 @@ let compute_proof_name locality = function
       if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
 	 locality == Global && Nametab.exists_cci (Lib.make_path_except_section id)
       then
-        user_err ~loc "" (pr_id id ++ str " already exists.");
+        user_err ~loc  (pr_id id ++ str " already exists.");
       id, pl
   | None ->
       next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
@@ -331,7 +331,7 @@ let get_proof proof do_guard hook opacity =
 let check_exist =
   List.iter (fun (loc,id) ->
     if not (Nametab.exists_cci (Lib.make_path id)) then
-        user_err ~loc "" (pr_id id ++ str " does not exist.")
+        user_err ~loc  (pr_id id ++ str " does not exist.")
   )
 
 let universe_proof_terminator compute_guard hook =
diff --git a/stm/stm.ml b/stm/stm.ml
index ff4688480..7c5a3bc6a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1038,7 +1038,7 @@ end = struct (* {{{ *)
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
-       CErrors.user_err "undo_vernac_classifier"
+       CErrors.user_err ~hdr:"undo_vernac_classifier"
         (str "Cannot undo")
 
 end (* }}} *)
@@ -1106,7 +1106,7 @@ let proof_block_delimiters = ref []
 
 let register_proof_block_delimiter name static dynamic =
   if List.mem_assoc name !proof_block_delimiters then
-    CErrors.user_err "STM" (str "Duplicate block delimiter " ++ str name);
+    CErrors.user_err ~hdr:"STM" (str "Duplicate block delimiter " ++ str name);
   proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters
 
 let mk_doc_node id = function
@@ -1141,7 +1141,7 @@ let detect_proof_block id name =
           VCS.create_proof_block decl name
       end
     with Not_found ->
-      CErrors.user_err "STM"
+      CErrors.user_err ~hdr:"STM"
         (str "Unknown proof block delimiter " ++ str name)
   )
 (****************************** THE SCHEDULER *********************************)
@@ -1706,7 +1706,7 @@ end = struct (* {{{ *)
          List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0))
                       Evd.(evar_context g))
        then
-         CErrors.user_err "STM" (strbrk("the par: goal selector supports ground "^
+         CErrors.user_err ~hdr:"STM" (strbrk("the par: goal selector supports ground "^
            "goals only"))
        else begin
         let (i, ast) = r_ast in
@@ -1719,7 +1719,7 @@ end = struct (* {{{ *)
             let t = Evarutil.nf_evar sigma t in
             if Evarutil.is_ground_term sigma t then
               RespBuiltSubProof (t, Evd.evar_universe_context sigma)
-            else CErrors.user_err "STM" (str"The solution is not ground")
+            else CErrors.user_err ~hdr:"STM" (str"The solution is not ground")
        end) ()
     with e when CErrors.noncritical e -> RespError (CErrors.print e)
 
@@ -2056,7 +2056,7 @@ let known_state ?(redefine_qed=false) ~cache id =
            | _ -> assert false
         end
       with Not_found ->
-          CErrors.user_err "STM"
+          CErrors.user_err ~hdr:"STM"
             (str "Unknown proof block delimiter " ++ str name)
   in
 
@@ -2405,7 +2405,7 @@ let handle_failure (e, info) vcs tty =
 let snapshot_vio ldir long_f_dot_vo =
   finish ();
   if List.length (VCS.branches ()) > 1 then
-    CErrors.user_err "stm" (str"Cannot dump a vio with open proofs");
+    CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs");
   Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
     (Global.opaque_tables ())
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index b898ceb04..7628b7885 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 ->
-    user_err "AutoRewrite"
+    user_err ~hdr:"AutoRewrite"
       (str "Rewriting base " ++ str bas ++ str " does not exist.")
 
 let find_rewrites bas =
@@ -294,7 +294,7 @@ let find_applied_relation metas loc env sigma c left2right =
     match decompose_applied_relation metas env sigma c ctype left2right with
     | Some c -> c
     | None ->
-	user_err ~loc "decompose_applied_relation"
+	user_err ~loc ~hdr:"decompose_applied_relation"
 		    (str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++
 		       spc () ++ str"of this term does not end with an applied relation.")
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index dcf3dea10..6308ab259 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -97,8 +97,8 @@ let prolog_tac l n =
   in
   let l = List.map map l in
   try (prolog l n gl)
-  with UserError ("Refiner.tclFIRST",_) ->
-    user_err "Prolog.prolog" (str "Prolog failed.")
+  with UserError (Some "Refiner.tclFIRST",_) ->
+    user_err ~hdr:"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 -> user_err "autounfold" (str "Unknown database " ++ str dbname)
+      with Not_found -> user_err ~hdr:"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 -> user_err "autounfold" (str "Unknown database " ++ str dbname)
+	with Not_found -> user_err ~hdr:"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 4391a96b1..24abd1e12 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 -> 
-	      user_err "Equality.find_elim"
+	      user_err ~hdr:"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
        *)
-      user_err "Equality.construct_discriminator"
+      user_err ~hdr:"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
-     | _  -> user_err "" (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 ->
-       user_err "DiscrEverywhere" (str"No discriminable equalities."))
+       user_err ~hdr:"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;
-          user_err "Subst"
+          user_err ~hdr:"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 e706316d7..841f35e9c 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 =
-  user_err "Hints" (str "No such Hint database: " ++ str x ++ str ".")
+  user_err ~hdr:"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
-    user_err "Hint"
+    user_err ~hdr:"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
-      user_err "Hint"
+      user_err ~hdr:"Hint"
 	(pr_global ref ++ str" has " ++ int n ++ 
 	   str" arguments while the mode declares " ++ int (Array.length m'))
     else m'
@@ -1411,6 +1411,6 @@ let run_hint tac k = match !warn_hint with
   else Proofview.tclBIND (k tac.obj) (fun x -> warn tac x)
 | `STRICT ->
   if is_imported tac then k tac.obj
-  else Proofview.tclZERO (UserError ("", (str "Tactic failure.")))
+  else Proofview.tclZERO (UserError (None, (str "Tactic failure.")))
 
 let repr_hint h = h.obj
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index aee3bc45d..2b31695f6 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 ->
-      user_err "" (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 a7f5ded5b..1a0bee0b8 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
-	    user_err "make_inv_predicate"
+	    user_err ~hdr:"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.user_err "" 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 e83093b0c..4f52df99c 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 ->
-      user_err "inversion_scheme" (no_inductive_inconstr env sigma i)
+      user_err ~hdr:"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)));
   (*
-    user_err "lemma_inversion"
+    user_err ~hdr:"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
@@ -247,8 +247,8 @@ let add_inversion_lemma_exn na com comsort bool tac =
   try
     add_inversion_lemma na env sigma c sort bool tac
   with
-    |   UserError ("Case analysis",s) -> (* Reference to Indrec *)
-	  user_err "Inv needs Nodep Prop Set" s
+    |   UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
+	  user_err ~hdr:"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 ->
-	user_err ""
+	user_err 
 	  (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma."))
     | UserError (a,b) ->
-	 user_err "LemInv"
+	 user_err ~hdr:"LemInv"
 	   (str "Cannot refine current goal with the lemma " ++
 	      pr_lconstr_env (Refiner.pf_env gls) (Refiner.project gls) c)
 
diff --git a/tactics/tactic_matching.ml b/tactics/tactic_matching.ml
index 004492e78..4d4ca7d9e 100644
--- a/tactics/tactic_matching.ml
+++ b/tactics/tactic_matching.ml
@@ -103,7 +103,7 @@ let verify_metas_coherence env sigma (ln1,lcm) (ln,lm) =
   (merged, Id.Map.merge merge lcm lm)
 
 let matching_error =
-  CErrors.UserError ("tactic matching" , Pp.str "No matching clauses for match.")
+  CErrors.UserError (Some "tactic matching" , Pp.str "No matching clauses for match.")
 
 let imatching_error = (matching_error, Exninfo.null)
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index c9af1f11c..9c2dd3fee 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -172,14 +172,14 @@ let check_or_and_pattern_size check_and loc names branchsigns =
   let n = Array.length branchsigns in
   let msg p1 p2 = strbrk "a conjunctive pattern made of " ++ int p1 ++ (if p1 == p2 then mt () else str " or " ++ int p2) ++ str " patterns" in
   let err1 p1 p2 =
-    user_err ~loc "" (str "Expects " ++ msg p1 p2 ++ str ".") in
+    user_err ~loc  (str "Expects " ++ msg p1 p2 ++ str ".") in
   let errn n =
-    user_err ~loc "" (str "Expects a disjunctive pattern with " ++ int n
+    user_err ~loc  (str "Expects a disjunctive pattern with " ++ int n
 	++ str " branches.") in
   let err1' p1 p2 =
-    user_err ~loc "" (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
+    user_err ~loc  (strbrk "Expects a disjunctive pattern with 1 branch or " ++ msg p1 p2 ++ str ".") in
   let errforthcoming loc =
-    user_err ~loc "" (strbrk "Unexpected non atomic pattern.") in
+    user_err ~loc  (strbrk "Unexpected non atomic pattern.") in
   match names with
   | IntroAndPattern l ->
       if not (Int.equal n 1) then errn n;
@@ -311,7 +311,7 @@ module New = struct
     tclZERO (Refiner.FailError (lvl,lazy msg))
 
   let tclZEROMSG ?loc msg =
-    let err = UserError ("", msg) in
+    let err = UserError (None, msg) in
     let info = match loc with
     | None -> Exninfo.null
     | Some loc -> Loc.add_loc Exninfo.null loc
@@ -643,7 +643,7 @@ module New = struct
 	    | Var id -> string_of_id id
 	    | _ -> "\b"
 	  in
-	  user_err "Tacticals.general_elim_then_using"
+	  user_err ~hdr:"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 16643b6a7..96dc8a2e2 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
-      user_err "Tactics.introduction"
+      user_err ~hdr:"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 =
-  user_err "" (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 =
-  user_err "" (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.user_err "" (pr_id elt ++ str " is already used")
+          CErrors.user_err  (pr_id elt ++ str " is already used")
         with Not_found -> ()
       in
       (** All is well *)
@@ -423,7 +423,7 @@ let find_name mayrepl decl naming gl = match naming with
       let ids_of_hyps = Tacmach.New.pf_ids_of_hyps gl in
       let id' = next_ident_away id ids_of_hyps in
       if not mayrepl && not (Id.equal id' id) then
-        user_err ~loc "" (pr_id id ++ str" is already used.");
+        user_err ~loc  (pr_id id ++ str" is already used.");
       id
 
 (**************************************************************)
@@ -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
-      user_err "Logic.prim_refiner"
+      user_err ~hdr:"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
-	user_err "" (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
-	user_err "" (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
-	user_err "" (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
-        user_err "convert-check-hyp" (str "Types are incompatible.")
+        user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.")
     else sigma
   end
   else
     if not (isSort (whd_all env sigma t1)) then
-      user_err "convert-check-hyp" (str "Not a type.")
+      user_err ~hdr:"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 user_err "convert-check-hyp" (str "Not convertible.");
+  if not b then user_err ~hdr:"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]
-  | _ -> user_err "unfold_constr" (str "Cannot unfold a non-constant.")
+  | _ -> user_err ~hdr:"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 ->
-        user_err "lookup_quantified_hypothesis"
+        user_err ~hdr:"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 user_err "" (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
-       | _  -> user_err "elimination_clause"
+       | _  -> user_err ~hdr:"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 _ -> user_err "elimination_clause"
+    with Failure _ -> user_err ~hdr:"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
-    user_err "general_rewrite_in"
+    user_err ~hdr:"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
-        user_err "" (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) ->
-	user_err "Tactics.check_number_of_constructors"
+	user_err ~hdr:"Tactics.check_number_of_constructors"
           (str "Not an inductive goal with " ++ int n ++ str (String.plural n " constructor") ++ str ".")
     | _ -> ()
   end;
@@ -2235,7 +2235,7 @@ let error_unexpected_extra_pattern loc bound pat =
   | IntroNaming (IntroIdentifier _) ->
       "name", (String.plural nb " introduction pattern"), "no"
   | _ -> "introduction pattern", "", "none" in
-  user_err ~loc "" (str "Unexpected " ++ str s1 ++ str " (" ++
+  user_err ~loc  (str "Unexpected " ++ str s1 ++ str " (" ++
     (if Int.equal nb 0 then (str s3 ++ str s2) else
       (str "at most " ++ int nb ++ str s2)) ++ spc () ++
        str (if Int.equal nb 1 then "was" else "were") ++
@@ -2475,7 +2475,7 @@ and prepare_intros_loc loc with_evars dft destopt = function
           (fun _ l -> clear_wildcards l) in
       fun id ->
         intro_pattern_action loc with_evars true true ipat [] destopt tac id)
-  | IntroForthcoming _ -> user_err ~loc ""
+  | IntroForthcoming _ -> user_err ~loc 
       (str "Introduction pattern for one hypothesis expected.")
 
 let intro_patterns_bound_to with_evars n destopt =
@@ -2643,7 +2643,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env
       | IntroIdentifier id ->
           if List.mem id (ids_of_named_context (named_context env)) then
-            user_err ~loc "" (pr_id id ++ str" is already used.");
+            user_err ~loc  (pr_id id ++ str" is already used.");
           id in
       let eqdata = build_coq_eq_data () in
       let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in
@@ -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
-	user_err "" (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
-	user_err "" (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 _ -> user_err "unfold_body"
+  | LocalAssum _ -> user_err ~hdr:"unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
   | LocalDef (_,xval,_) -> xval
   in
@@ -3028,7 +3028,7 @@ let safe_dest_intro_patterns with_evars avoid thin dest pat tac =
   Proofview.tclORELSE
     (dest_intro_patterns with_evars avoid thin dest pat tac)
     begin function (e, info) -> match e with
-      | UserError ("move_hyp",_) ->
+      | UserError (Some "move_hyp",_) ->
        (* May happen e.g. with "destruct x using s" with an hypothesis
           which is morally an induction hypothesis to be "MoveLast" if
           known as such but which is considered instead as a subterm of
@@ -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
-  user_err "Tactics" (str "Cannot recognize " ++ str s ++ str "an induction scheme.")
+  user_err ~hdr:"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
-	  | _  -> user_err "elimination_clause"
+	  | _  -> user_err ~hdr:"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 user_err ""
+  then user_err 
     (str "Conclusion must be mentioned: it depends on " ++ pr_id id
      ++ str ".");
   match cls.onhyps with
@@ -4392,7 +4392,7 @@ let induction_gen_l isrec with_evars elim names lc =
   let lc = List.map (function
     | (c,None) -> c
     | (c,Some(loc,eqname)) ->
-      user_err ~loc "" (str "Do not know what to do with " ++
+      user_err ~loc  (str "Do not know what to do with " ++
                          Miscprint.pr_intro_pattern_naming eqname)) lc in
   let rec atomize_list l =
     match l with
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index a7c32e1d6..a9f1b7376 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -526,5 +526,5 @@ let _ =
   try
     coqdep ()
   with CErrors.UserError(s,p) ->
-    let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in
+    let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p))  in
     Feedback.msg_error pp
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index d6c2ccad2..4f3eeda3a 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 user_err "AutoIndDecl.do_replace_lb"
+            else user_err ~hdr:"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 user_err "AutoIndDecl.do_replace_bl"
+            else user_err ~hdr:"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 -> user_err "AutoIndDecl.eqI"
+    with Not_found -> user_err ~hdr:"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
-    user_err ""
+    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
-    user_err ""
+    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 bf17867e8..0dc799014 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 ->
-      user_err "class_of_global"
+      user_err ~hdr:"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 =
-  user_err "build_id_coercion"
+  user_err ~hdr:"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
-      user_err "" (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 ->
-      user_err "try_add_new_coercion_core"
+      user_err ~hdr:"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 6d62ce24a..cff744534 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -66,8 +66,9 @@ let existing_instance glob g pri =
     match class_of_constr r with
       | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob 
   (*FIXME*) (Flags.use_polymorphic_flag ()) c)
-      | None -> user_err ~loc:(loc_of_reference g) "declare_instance"
-			    (Pp.str "Constant does not build instances of a declared type class.")
+      | None -> user_err ~loc:(loc_of_reference g)
+                         ~hdr:"declare_instance"
+                         (Pp.str "Constant does not build instances of a declared type class.")
 
 let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
 let mismatched_props env n m = mismatched_ctx_inst env Properties n m
@@ -169,7 +170,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
-	      user_err "new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
+	      user_err ~hdr:"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 4d333c30d..c8e0d1637 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -57,7 +57,7 @@ let rec complete_conclusion a cs = function
   | CHole (loc, k, _, _) ->
       let (has_no_args,name,params) = a in
       if not has_no_args then
-	user_err ~loc ""
+	user_err ~loc 
 	 (strbrk"Cannot infer the non constant arguments of the conclusion of "
 	  ++ pr_id cs ++ str ".");
       let args = List.map (fun id -> CRef(Ident(loc,id),None)) params in
@@ -330,7 +330,7 @@ let do_assumptions kind nl l = match l with
   | (Discharge, _, _) when Lib.sections_are_opened () ->
     let loc = fst id in
     let msg = Pp.str "Section variables cannot be polymorphic." in
-    user_err ~loc "" msg
+    user_err ~loc  msg
   | _ -> ()
   in
   do_assumptions_bound_univs coe kind nl id (Some pl) c
@@ -342,7 +342,7 @@ let do_assumptions kind nl l = match l with
       let loc = fst id in
       let msg =
 	Pp.str "Assumptions with bound universes can only be defined one at a time." in
-      user_err ~loc "" msg
+      user_err ~loc  msg
     in
     (coe, (List.map map idl, c))
   in
@@ -438,7 +438,7 @@ let interp_ind_arity env evdref ind =
   let t, impls = understand_tcc_evars env evdref ~expected_type:IsType c, imps in
   let pseudo_poly = check_anonymous_type c in
   let () = if not (Reduction.is_arity env t) then
-    user_err ~loc:(constr_loc ind.ind_arity) "" (str "Not an arity")
+    user_err ~loc:(constr_loc ind.ind_arity) (str "Not an arity")
   in
     t, pseudo_poly, impls
 
@@ -553,7 +553,7 @@ let check_named (loc, na) = match na with
 | Name _ -> ()
 | Anonymous ->
   let msg = str "Parameters must be named." in
-  user_err ~loc "" msg
+  user_err ~loc  msg
 
 
 let check_param = function
@@ -955,7 +955,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let relargty =
     let error () =
       user_err ~loc:(constr_loc r)
-		    "Command.build_wellfounded"
+               ~hdr:"Command.build_wellfounded"
 		    (Printer.pr_constr_env env !evdref rel ++ str " is not an homogeneous binary relation.")
     in
       try
@@ -1312,7 +1312,7 @@ let do_program_fixpoint local poly l =
 	  match n with
 	  | Some n -> mkIdentC (snd n)
 	  | None ->
-	      user_err "do_program_fixpoint"
+	      user_err ~hdr:"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
 
     | _, _ ->
-	user_err "do_program_fixpoint"
+	user_err ~hdr:"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 b90e62048..59ee95b31 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.user_err "get_compat_version"
+    CErrors.user_err ~hdr:"get_compat_version"
       (str "Compatibility with version " ++ str s ++ str " not supported.")
-  | s -> CErrors.user_err "get_compat_version"
+  | s -> CErrors.user_err ~hdr:"get_compat_version"
       (str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index fee5cffeb..85d0b6194 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*)
-    user_err "IndTables.declare_scheme_object"
+    user_err ~hdr:"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/indschemes.ml b/toplevel/indschemes.ml
index f9e6c207c..e0b861e0a 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -193,7 +193,7 @@ let try_declare_scheme what f internal names kn =
   in
   match msg with
   | None -> ()
-  | Some msg -> iraise (UserError ("", msg), snd e)
+  | Some msg -> iraise (UserError (None, msg), snd e)
 
 let beq_scheme_msg mind =
   let mib = Global.lookup_mind mind in
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index 7664acbb6..03640676e 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.user_err "Locality.check_locality"
+    CErrors.user_err ~hdr:"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 cef074699..cd244bf63 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 :: _, _ ->
-      user_err "Metasyntax.find_pattern"
+      user_err ~hdr:"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
-	  user_err "Metasyntax.get_notation_vars"
+	  user_err ~hdr:"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 =
-  user_err "Metasyntax.error_not_name_scope"
+  user_err ~hdr:"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
-    user_err "" (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 =
-  user_err ""
+  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
-	  user_err "Metasyntax.interp_modifiers"
+	  user_err ~hdr:"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
-	  user_err "Metasyntax.interp_modifiers"
+	  user_err ~hdr:"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,_)::_ -> user_err "Metasyntax.check_useless_entry_types"
+  | (x,_)::_ -> user_err ~hdr:"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 ->
-	user_err ""
+	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 c74c3522d..f9e0bc34a 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
-            user_err "Mltop.load_object" (str"Cannot link ml-object " ++
+            user_err ~hdr:"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 ->
-          user_err "Mltop.load_object"
+          user_err ~hdr:"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
-      user_err "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
+      user_err ~hdr:"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 =
-    user_err "Mltop.load_object"
+    user_err ~hdr:"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
-    user_err "Mltop.trigger_ml_object"
+    user_err ~hdr:"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 b9fd2894d..91704585a 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.user_err "Program" cmd
+let pperror cmd = CErrors.user_err ~hdr:"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
     | _ ->
-	user_err "prod_app"
+	user_err ~hdr:"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
-      user_err "Program" 
+      user_err ~hdr:"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
-                user_err ""
+                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 "\""))
 
@@ -985,7 +985,7 @@ and solve_obligation_by_tac prg obls i tac =
           let (e, _) = CErrors.push e in
           match e with
 	  | Refiner.FailError (_, s) ->
-	      user_err ~loc:(fst obl.obl_location) "solve_obligation" (Lazy.force s)
+	      user_err ~loc:(fst obl.obl_location) ~hdr:"solve_obligation" (Lazy.force s)
           | e -> None (* FIXME really ? *)
 
 and solve_prg_obligations prg ?oblset tac =
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 22dc8c957..219f078e1 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -102,7 +102,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
     let error bk (loc, name) = 
       match bk, name with
       | Default _, Anonymous ->
-        user_err ~loc "record" (str "Record parameters must be named")
+        user_err ~loc ~hdr:"record" (str "Record parameters must be named")
       | _ -> ()
     in
       List.iter 
@@ -127,7 +127,7 @@ let typecheck_params_and_fields def id pl t ps nots fs =
 	                  sred, true
 	       | None -> s, false
              else s, false)
-	 | _ -> user_err ~loc:(constr_loc t) "" (str"Sort expected."))
+	 | _ -> user_err ~loc:(constr_loc t) (str"Sort expected."))
     | None -> 
       let uvarkind = Evd.univ_flexible_alg in
 	mkSort (Evarutil.evd_comb0 (Evd.new_sort_variable uvarkind) evars), true
@@ -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 user_err "structure" st;
+  if coe then user_err ~hdr:"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 ->
-                user_err "" (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
@@ -539,7 +539,7 @@ let declare_existing_class g =
   match g with
   | ConstRef x -> add_constant_class x
   | IndRef x -> add_inductive_class x
-  | _ -> user_err "declare_existing_class"
+  | _ -> user_err ~hdr:"declare_existing_class"
 		      (Pp.str"Unsupported class type, only constants and inductives are allowed")
 
 open Vernacexpr
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 00655497b..d345b3229 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -70,7 +70,7 @@ let disable_drop = function
   | Drop -> CErrors.error "Drop is forbidden."
   | e -> e
 
-let user_error loc s = CErrors.user_err ~loc "_" (str s)
+let user_error loc s = CErrors.user_err ~loc ~hdr:"_" (str s)
 
 (* Opening and closing a channel. Open it twice when verbose: the first
    channel is used to read the commands, and the second one to print them.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9e3494145..3dd19fa1d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -381,7 +381,7 @@ let err_unmapped_library loc ?from qid =
     str " and prefix " ++ pr_dirpath from ++ str "."
   in
   user_err ~loc
-    "locate_library"
+    ~hdr:"locate_library"
     (strbrk "Cannot find a physical path bound to logical path matching suffix " ++
        pr_dirpath dir ++ prefix)
 
@@ -391,7 +391,7 @@ let err_notfound_library loc ?from qid =
   | Some from ->
     str " with prefix " ++ pr_dirpath from ++ str "."
   in
-  user_err ~loc "locate_library"
+  user_err ~loc ~hdr:"locate_library"
      (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix)
 
 let print_located_library r =
@@ -483,7 +483,7 @@ let vernac_start_proof locality p kind l lettop =
 	| None -> ()) l;
   if not(refining ()) then
     if lettop then
-      user_err "Vernacentries.StartProof"
+      user_err ~hdr:"Vernacentries.StartProof"
 	(str "Let declarations can only be used in proof editing mode.");
   start_proof_and_print (local, p, Proof kind) l no_hook
 
@@ -604,14 +604,14 @@ let vernac_combined_scheme lid l =
 
 let vernac_universe loc poly l =
   if poly && not (Lib.sections_are_opened ()) then
-    user_err ~loc "vernac_universe"
+    user_err ~loc ~hdr:"vernac_universe"
 		 (str"Polymorphic universes can only be declared inside sections, " ++
 		  str "use Monomorphic Universe instead");
   do_universe poly l
 
 let vernac_constraint loc poly l =
   if poly && not (Lib.sections_are_opened ()) then
-    user_err ~loc "vernac_constraint"
+    user_err ~loc ~hdr:"vernac_constraint"
 		 (str"Polymorphic universe constraints can only be declared"
 		  ++ str " inside sections, use Monomorphic Constraint instead");
   do_constraint poly l
@@ -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
-      user_err "vernac_set_used_variables"
+      user_err ~hdr:"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::_, _ -> user_err "vernac_declare_arguments"
+    | [], x::_, _ -> user_err ~hdr:"vernac_declare_arguments"
                        (str "Extra argument " ++ pr_name x ++ str ".")
-    | l, [], _ -> user_err "vernac_declare_arguments"
+    | l, [], _ -> user_err ~hdr:"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 ->
-            user_err "vernac_declare_arguments"
+            user_err ~hdr:"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
-      user_err "vernac_declare_arguments"
+      user_err ~hdr:"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)
-    | _ -> user_err "" (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 _ -> user_err "print_about_hyp_globs"
+	    Failure _ -> user_err ~hdr:"print_about_hyp_globs"
                            (str "No such goal: " ++ int n ++ str "."))
       | _ , _ -> raise NoHyp in
     let hyps = pf_hyps gl in
@@ -1574,7 +1574,7 @@ let global_module r =
   let (loc,qid) = qualid_of_reference r in
   try Nametab.full_name_module qid
   with Not_found ->
-    user_err ~loc "global_module"
+    user_err ~loc ~hdr:"global_module"
      (str "Module/section " ++ pr_qualid qid ++ str " not found.")
 
 let interp_search_restriction = function
@@ -1597,7 +1597,7 @@ let interp_search_about_item env =
 	    (fun _ -> true) s sc in
 	GlobSearchSubPattern (Pattern.PRef ref)
       with UserError _ ->
-	user_err "interp_search_about_item"
+	user_err ~hdr:"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.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")
+  | 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 ->
-          user_err "Fail" (str "The command has not failed!")
+          user_err ~hdr:"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 147727e7c..f26ef460d 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 _ ->
-    user_err "vinterp_add"
+    user_err ~hdr:"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 ->
-    user_err "Vernac Interpreter"
+    user_err ~hdr:"Vernac Interpreter"
       (str"Cannot find vernac command " ++ str (fst s) ++ str".")
 
 let vinterp_init () = Hashtbl.clear vernac_tab