Merge PR#512: [cleanup] Unify all calls to the error function.

1 files changed, 8 insertions, 7 deletions

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 0cb72cc3a..38f05978d 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