Make the user_err header an optional parameter.

Suggested by @ppedrot

11 files changed, 61 insertions, 61 deletions

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