[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, 7 insertions, 8 deletions

diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 470a93f2b..bf84f61a5 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -56,17 +56,16 @@ let instantiate_tac n c ido =
 		InHyp ->
 		  (match decl with
                     | LocalAssum (_,typ) -> evar_list sigma (EConstr.of_constr typ)
-		    | _ -> error
-			"Please be more specific: in type or value?")
+		    | _ -> user_err Pp.(str "Please be more specific: in type or value?"))
 	      | InHypTypeOnly ->
 		  evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl))
 	      | InHypValueOnly ->
 		  (match decl with
 		    | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body)
-		    | _ -> error "Not a defined hypothesis.") in
+		    | _ -> user_err Pp.(str "Not a defined hypothesis.")) in
   if List.length evl < n then
-    error "Not enough uninstantiated existential variables.";
-  if n <= 0 then error "Incorrect existential variable index.";
+    user_err Pp.(str "Not enough uninstantiated existential variables.");
+  if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
   let evk,_ = List.nth evl (n-1) in
   instantiate_evar evk c sigma gl
   end
@@ -76,7 +75,7 @@ let instantiate_tac_by_name id c =
   let sigma = gl.sigma in
   let evk =
     try Evd.evar_key id sigma
-    with Not_found -> error "Unknown existential variable." in
+    with Not_found -> user_err Pp.(str "Unknown existential variable.") in
   instantiate_evar evk c sigma gl
   end
 
@@ -109,8 +108,8 @@ let hget_evar n =
   let concl = Proofview.Goal.concl gl in
   let evl = evar_list sigma concl in
   if List.length evl < n then
-    error "Not enough uninstantiated existential variables.";
-  if n <= 0 then error "Incorrect existential variable index.";
+    user_err Pp.(str "Not enough uninstantiated existential variables.");
+  if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
   let ev = List.nth evl (n-1) in
   let ev_type = EConstr.existential_type sigma ev in
   Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))