From b1d749e59444f86e40f897c41739168bb1b1b9b3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 25 Feb 2018 22:43:42 +0100 Subject: [located] Push inner locations in `reference` to a CAst.t node. The `reference` type contains some ad-hoc locations in its constructors, but there is no reason not to handle them with the standard attribute container provided by `CAst.t`. An orthogonal topic to this commit is whether the `reference` type should contain a location or not at all. It seems that many places would become a bit clearer by splitting `reference` into non-located `reference` and `lreference`, however some other places become messier so we maintain the current status-quo for now. --- library/nametab.ml | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) (limited to 'library/nametab.ml') diff --git a/library/nametab.ml b/library/nametab.ml index 0e996443f..2046bf758 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -18,8 +18,8 @@ open Globnames exception GlobalizationError of qualid -let error_global_not_found ?loc q = - Loc.raise ?loc (GlobalizationError q) +let error_global_not_found {CAst.loc;v} = + Loc.raise ?loc (GlobalizationError v) (* The visibility can be registered either - for all suffixes not shorter then a given int - when the object @@ -459,16 +459,16 @@ let global_of_path sp = let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab -let global r = - let (loc,qid) = qualid_of_reference r in - try match locate_extended qid with +let global ({CAst.loc;v=r} as lr)= + let {CAst.loc; v} as qid = qualid_of_reference lr in + try match locate_extended v with | TrueGlobal ref -> ref | SynDef _ -> user_err ?loc ~hdr:"global" (str "Unexpected reference to a notation: " ++ - pr_qualid qid) + pr_qualid v) with Not_found -> - error_global_not_found ?loc qid + error_global_not_found qid (* Exists functions ********************************************************) @@ -539,13 +539,12 @@ let pr_global_env env ref = with Not_found as e -> if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e -let global_inductive r = - match global r with +let global_inductive ({CAst.loc; v=r} as lr) = + match global lr with | IndRef ind -> ind | ref -> - user_err ?loc:(loc_of_reference r) ~hdr:"global_inductive" - (pr_reference r ++ spc () ++ str "is not an inductive type") - + user_err ?loc ~hdr:"global_inductive" + (pr_reference lr ++ spc () ++ str "is not an inductive type") (********************************************************************) -- cgit v1.2.3