Unify location handling of error functions.

In some cases prior to this patch, there were two cases for the same
error function, one taking a location, the other not.

We unify them by using an option parameter, in the line with recent
changes in warnings and feedback.

This implies a bit of clean up in some places, but more importantly, is
the preparation for subsequent patches making `Loc.location` opaque,
change that could be use to improve modularity and allow a more
functional implementation strategy --- for example --- of the
beautifier.

4 files changed, 20 insertions, 23 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 3d063225f..f8c3cddc4 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -462,8 +462,8 @@ let do_universe poly l =
   let in_section = Lib.sections_are_opened () in
   let () =
     if poly && not in_section then
-      user_err_loc (Loc.ghost, "Constraint",
-                    str"Cannot declare polymorphic universes outside sections")
+      user_err "Constraint"
+                   (str"Cannot declare polymorphic universes outside sections")
   in
   let l =
     List.map (fun (l, id) ->
@@ -496,20 +496,20 @@ let do_constraint poly l =
     fun (loc, id) ->
     try Idmap.find id names
     with Not_found ->
-      user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id)
+      user_err ~loc "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_loc (Loc.ghost, "Constraint",
-                    str"Cannot declare polymorphic constraints outside sections")
+      user_err "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 (loc, "Constraint",
-                    str "Cannot declare a global constraint on " ++
+      user_err ~loc "Constraint"
+                    (str "Cannot declare a global constraint on " ++
                     str "a polymorphic universe, use "
                     ++ str "Polymorphic Constraint instead")
   in
diff --git a/library/library.ml b/library/library.ml
index 12090183a..0d65b3d0a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -572,8 +572,8 @@ let require_library_from_dirpath modrefl export =
 let safe_locate_module (loc,qid) =
   try Nametab.locate_module qid
   with Not_found ->
-    user_err_loc
-      (loc,"import_library", pr_qualid qid ++ str " is not a module")
+    user_err ~loc "import_library"
+      (pr_qualid qid ++ str " is not a module")
 
 let import_module export modl =
   (* Optimization: libraries in a raw in the list are imported
@@ -597,8 +597,8 @@ let import_module export modl =
             flush acc;
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
-              user_err_loc (loc,"import_library",
-                pr_qualid dir ++ str " is not a module"))
+              user_err ~loc "import_library"
+                (pr_qualid dir ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
diff --git a/library/nametab.ml b/library/nametab.ml
index fa5db37ed..989dcf3f3 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -16,10 +16,8 @@ open Globnames
 
 exception GlobalizationError of qualid
 
-let error_global_not_found_loc loc q =
-  Loc.raise loc (GlobalizationError q)
-
-let error_global_not_found q = raise (GlobalizationError q)
+let error_global_not_found ?loc q =
+  Loc.raise ?loc (GlobalizationError q)
 
 (* Kinds of global names *)
 
@@ -455,11 +453,11 @@ let global r =
   try match locate_extended qid with
     | TrueGlobal ref -> ref
     | SynDef _ ->
-        user_err_loc (loc,"global",
-          str "Unexpected reference to a notation: " ++
-          pr_qualid qid)
+        user_err ~loc "global"
+          (str "Unexpected reference to a notation: " ++
+           pr_qualid qid)
   with Not_found ->
-    error_global_not_found_loc loc qid
+    error_global_not_found ~loc qid
 
 (* Exists functions ********************************************************)
 
@@ -534,8 +532,8 @@ let global_inductive r =
   match global r with
   | IndRef ind -> ind
   | ref ->
-      user_err_loc (loc_of_reference r,"global_inductive",
-        pr_reference r ++ spc () ++ str "is not an inductive type")
+      user_err ~loc:(loc_of_reference r) "global_inductive"
+        (pr_reference r ++ spc () ++ str "is not an inductive type")
 
 
 (********************************************************************)
diff --git a/library/nametab.mli b/library/nametab.mli
index a8a0572b3..d20c399b6 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -60,8 +60,7 @@ open Globnames
 exception GlobalizationError of qualid
 
 (** Raises a globalization error *)
-val error_global_not_found_loc : Loc.t -> qualid -> 'a
-val error_global_not_found     : qualid -> 'a
+val error_global_not_found : ?loc:Loc.t -> qualid -> 'a
 
 (** {6 Register visibility of things } *)