diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-06-19 16:48:12 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-06-19 16:48:12 +0200 |
commit | 6715e6801c1d285a12eeca55dd8b831d7efb8c0d (patch) | |
tree | 2b8925708d85f7cef5fb222d551cf809704f8ebd /interp/smartlocate.ml | |
parent | c37881f3d64a6db0d7414eb18adfa4de6b64d4b1 (diff) | |
parent | 133ac4fbb9a8b4213cb3f8ca2f7c2568931209ce (diff) |
Merge PR #7797: Remove reference name type.
Diffstat (limited to 'interp/smartlocate.ml')
-rw-r--r-- | interp/smartlocate.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index e1fbdba87..91491bdf8 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -41,26 +41,24 @@ let global_of_extended_global = function | [],NApp (NRef ref,[]) -> ref | _ -> raise Not_found -let locate_global_with_alias ?(head=false) {CAst.loc; v=qid} = +let locate_global_with_alias ?(head=false) qid = let ref = Nametab.locate_extended qid in try if head then global_of_extended_global_head ref else global_of_extended_global ref with Not_found -> - user_err ?loc (pr_qualid qid ++ + user_err ?loc:qid.CAst.loc (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") -let global_inductive_with_alias ({CAst.loc} as lr) = - let qid = qualid_of_reference lr in +let global_inductive_with_alias qid = try match locate_global_with_alias qid with | IndRef ind -> ind | ref -> - user_err ?loc ~hdr:"global_inductive" - (pr_reference lr ++ spc () ++ str "is not an inductive type.") + user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" + (pr_qualid qid ++ spc () ++ str "is not an inductive type.") with Not_found -> Nametab.error_global_not_found qid -let global_with_alias ?head r = - let qid = qualid_of_reference r in +let global_with_alias ?head qid = try locate_global_with_alias ?head qid with Not_found -> Nametab.error_global_not_found qid |