Make the user_err header an optional parameter.

Suggested by @ppedrot

19 files changed, 58 insertions, 58 deletions

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