From 8a807b2ffc27b84c9ea0ffe9f22b164ade24badb Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 15 Mar 2017 20:48:10 +0100 Subject: [cleanup] Unify all calls to the error function. This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated. --- plugins/setoid_ring/newring.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'plugins/setoid_ring/newring.ml') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e20e78b1a..0e1225ada 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -8,7 +8,6 @@ open Ltac_plugin open Pp -open CErrors open Util open Names open Term @@ -32,6 +31,8 @@ open Misctypes open Newring_ast open Proofview.Notations +let error msg = CErrors.user_err Pp.(str msg) + (****************************************************************************) (* controlled reduction *) @@ -46,7 +47,7 @@ let tag_arg tag_rec map subs i c = let global_head_of_constr sigma c = let f, args = decompose_app sigma c in try fst (Termops.global_of_constr sigma f) - with Not_found -> anomaly (str "global_head_of_constr") + with Not_found -> CErrors.anomaly (str "global_head_of_constr") let global_of_constr_nofail c = try global_of_constr c @@ -82,7 +83,7 @@ let add_map s m = protect_maps := String.Map.add s m !protect_maps let lookup_map map = try String.Map.find map !protect_maps with Not_found -> - user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") + CErrors.user_err ~hdr:"lookup_map" (str"map "++qs map++str"not found") let protect_red map env sigma c0 = let evars ev = Evarutil.safe_evar_value sigma ev in @@ -359,13 +360,13 @@ let find_ring_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - user_err ~hdr:"ring" + CErrors.user_err ~hdr:"ring" (str"arguments of ring_simplify do not have all the same type") in List.iter check cl'; (try ring_for_carrier (EConstr.to_constr sigma ty) with Not_found -> - user_err ~hdr:"ring" + CErrors.user_err ~hdr:"ring" (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false @@ -852,13 +853,13 @@ let find_field_structure env sigma l = let check c = let ty' = Retyping.get_type_of env sigma c in if not (Reductionops.is_conv env sigma ty ty') then - user_err ~hdr:"field" + CErrors.user_err ~hdr:"field" (str"arguments of field_simplify do not have all the same type") in List.iter check cl'; (try field_for_carrier (EConstr.to_constr sigma ty) with Not_found -> - user_err ~hdr:"field" + CErrors.user_err ~hdr:"field" (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) | [] -> assert false -- cgit v1.2.3