Make the user_err header an optional parameter.

Suggested by @ppedrot

8 files changed, 36 insertions, 36 deletions

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 ()