diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 15 |
1 files changed, 8 insertions, 7 deletions
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 |