[location] Make location optional in Loc.located

This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.

We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.

The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.

4 files changed, 11 insertions, 11 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 6b505ac09..3adb957fa 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -522,7 +522,7 @@ let do_constraint poly l =
        let names, _ = Global.global_universe_names () in
        try loc, Idmap.find id names
        with Not_found ->
-         user_err ~loc ~hdr:"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 () =
@@ -530,18 +530,18 @@ let do_constraint poly l =
       user_err ~hdr:"Constraint"
                     (str"Cannot declare polymorphic constraints outside sections")
   in
-  let check_poly loc p loc' p' =
+  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 ~hdr:"Constraint"
+      user_err ?loc ~hdr:"Constraint"
                     (str "Cannot declare a global constraint on " ++
                     str "a polymorphic universe, use "
                     ++ str "Polymorphic Constraint instead")
   in
   let constraints = List.fold_left (fun acc (l, d, r) ->
      let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in
-     check_poly ploc p rloc p';
+     check_poly ?loc:ploc p rloc p';
      Univ.Constraint.add (lu, d, ru) acc)
     Univ.Constraint.empty l
   in
diff --git a/library/libnames.mli b/library/libnames.mli
index 58d1da9d6..57013ef82 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -125,7 +125,7 @@ val eq_reference : reference -> reference -> bool
 val qualid_of_reference : reference -> qualid located
 val string_of_reference : reference -> string
 val pr_reference : reference -> std_ppcmds
-val loc_of_reference : reference -> Loc.t
+val loc_of_reference : reference -> Loc.t option
 val join_reference : reference -> reference -> reference
 
 (** Deprecated synonyms *)
diff --git a/library/library.ml b/library/library.ml
index 3086e3d18..2b3381fa7 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -582,7 +582,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 ~hdr:"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 =
     | [] -> ()
     | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
   let rec aux acc = function
-    | (loc,dir as m) :: l ->
+    | (loc, dir as m) :: l ->
         let m,acc =
           try Nametab.locate_module dir, acc
           with Not_found-> flush acc; safe_locate_module m, [] in
@@ -607,7 +607,7 @@ let import_module export modl =
             flush acc;
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
-              user_err ~loc ~hdr:"import_library"
+              user_err ?loc ~hdr:"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 b76048e89..1027e291c 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -453,11 +453,11 @@ let global r =
   try match locate_extended qid with
     | TrueGlobal ref -> ref
     | SynDef _ ->
-        user_err ~loc ~hdr:"global"
+        user_err ?loc ~hdr:"global"
           (str "Unexpected reference to a notation: " ++
            pr_qualid qid)
   with Not_found ->
-    error_global_not_found ~loc qid
+    error_global_not_found ?loc qid
 
 (* Exists functions ********************************************************)
 
@@ -532,7 +532,7 @@ let global_inductive r =
   match global r with
   | IndRef ind -> ind
   | ref ->
-      user_err ~loc:(loc_of_reference r) ~hdr:"global_inductive"
+      user_err ?loc:(loc_of_reference r) ~hdr:"global_inductive"
         (pr_reference r ++ spc () ++ str "is not an inductive type")