From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 18 Jan 2017 15:46:23 +0100 Subject: [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 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 and other times it printed nothing as the caller checked for `is_ghost` upstream. --- library/declare.ml | 8 ++++---- library/libnames.mli | 2 +- library/library.ml | 6 +++--- library/nametab.ml | 6 +++--- 4 files changed, 11 insertions(+), 11 deletions(-) (limited to 'library') 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") -- cgit v1.2.3