[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.

1 files changed, 5 insertions, 5 deletions

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 67221046b..3d41d2ddd 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -858,7 +858,7 @@ let try_red_product env sigma c =
 
 let red_product env sigma c =
   try try_red_product env sigma c
-  with Redelimination -> error "No head constant to reduce."
+  with Redelimination -> user_err (str "No head constant to reduce.")
 
 (*
 (* This old version of hnf uses betadeltaiota instead of itself (resp
@@ -1080,7 +1080,7 @@ let unfold env sigma name c =
   if is_evaluable env name then
     clos_norm_flags (unfold_red name) env sigma c
   else
-    error (string_of_evaluable_ref env name^" is opaque.")
+    user_err Pp.(str (string_of_evaluable_ref env name^" is opaque."))
 
 (* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
  * Unfolds the constant name in a term c following a list of occurrences occl.
@@ -1090,7 +1090,7 @@ let unfoldoccs env sigma (occs,name) c =
   let unfo nowhere_except_in locs =
     let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in
     if Int.equal nbocc 1 then
-      error ((string_of_evaluable_ref env name)^" does not occur.");
+      user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur."));
     let rest = List.filter (fun o -> o >= nbocc) locs in
     let () = match rest with
     | [] -> ()
@@ -1112,7 +1112,7 @@ let unfoldn loccname env sigma c =
 let fold_one_com com env sigma c =
   let rcom =
     try red_product env sigma com
-    with Redelimination -> error "Not reducible." in
+    with Redelimination -> user_err Pp.(str "Not reducible.") in
   (* Reason first on the beta-iota-zeta normal form of the constant as
      unfold produces it, so that the "unfold f; fold f" configuration works
      to refold fix expressions *)
@@ -1147,7 +1147,7 @@ let compute = cbv_betadeltaiota
 let abstract_scheme env sigma (locc,a) (c, sigma) =
   let ta = Retyping.get_type_of env sigma a in
   let na = named_hd env sigma ta Anonymous in
-  if occur_meta sigma ta then error "Cannot find a type for the generalisation.";
+  if occur_meta sigma ta then user_err Pp.(str "Cannot find a type for the generalisation.");
   if occur_meta sigma a then
     mkLambda (na,ta,c), sigma
   else