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. --- interp/smartlocate.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'interp/smartlocate.ml') diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index fd9599ec0..a9d94669a 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -46,7 +46,7 @@ let locate_global_with_alias ?(head=false) (loc,qid) = 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 (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") let global_inductive_with_alias r = @@ -54,27 +54,27 @@ let global_inductive_with_alias r = try match locate_global_with_alias lqid 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.") - with Not_found -> Nametab.error_global_not_found ~loc qid + with Not_found -> Nametab.error_global_not_found ?loc qid let global_with_alias ?head r = let (loc,qid as lqid) = qualid_of_reference r in try locate_global_with_alias ?head lqid - with Not_found -> Nametab.error_global_not_found ~loc qid + with Not_found -> Nametab.error_global_not_found ?loc qid let smart_global ?head = function | AN r -> global_with_alias ?head r | ByNotation (loc,(ntn,sc)) -> - Notation.interp_notation_as_global_reference ~loc (fun _ -> true) ntn sc + Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc let smart_global_inductive = function | AN r -> global_inductive_with_alias r | ByNotation (loc,(ntn,sc)) -> destIndRef - (Notation.interp_notation_as_global_reference ~loc isIndRef ntn sc) + (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc) let loc_of_smart_reference = function | AN r -> loc_of_reference r -- cgit v1.2.3