Make the user_err header an optional parameter.

Suggested by @ppedrot

4 files changed, 8 insertions, 8 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 7ee342ea0b..15654b4c6f 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 e14a2bd396..6e821ea5aa 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 c47c44e222..51b3a7260a 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 c82c30400b..c66af02bb9 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) ++