From de038270f72214b169d056642eb7144a79e6f126 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 7 Jul 2016 04:56:24 +0200 Subject: Unify location handling of error functions. In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier. --- interp/reserve.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'interp/reserve.ml') diff --git a/interp/reserve.ml b/interp/reserve.ml index 388ca0805..31425fb98 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -86,13 +86,13 @@ let in_reserved : Id.t * notation_constr -> obj = let declare_reserved_type_binding (loc,id) t = if not (Id.equal id (root_of_id id)) then - user_err_loc(loc,"declare_reserved_type", - (pr_id id ++ str + user_err ~loc "declare_reserved_type" + ((pr_id id ++ str " is not reservable: it must have no trailing digits, quote, or _")); begin try let _ = Id.Map.find id !reserve_table in - user_err_loc(loc,"declare_reserved_type", - (pr_id id++str" is already bound to a type")) + user_err ~loc "declare_reserved_type" + ((pr_id id++str" is already bound to a type")) with Not_found -> () end; add_anonymous_leaf (in_reserved (id,t)) -- cgit v1.2.3