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

8 files changed, 29 insertions, 30 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))
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index a3310c2d8..fdb8d3461 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -90,7 +90,7 @@ let occurrences_of = function
   | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl)
   | nl ->
       if List.exists (fun n -> n < 0) nl then
-        CErrors.error "Illegal negative occurrence number.";
+        CErrors.user_err Pp.(str "Illegal negative occurrence number.");
       OnlyOccurrences nl
 
 let coerce_to_int v = match Value.to_int v with
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index cbd8a7f0f..ed80dd7ae 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -1084,7 +1084,7 @@ let decompose l c =
     let sigma = Tacmach.New.project gl in
     let to_ind c =
       if isInd sigma c then fst (destInd sigma c)
-      else error "not an inductive type"
+      else user_err Pp.(str "not an inductive type")
     in
     let l = List.map to_ind l in
     Elim.h_decompose l c
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 257100b01..1404b1c1f 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -117,8 +117,8 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
       | _, Some x ->
           let ids = List.map snd (List.flatten (List.map pi1 bl)) in
           (try List.index Names.Name.equal (snd x) ids
-          with Not_found -> error "No such fix variable.")
-      | _ -> error "Cannot guess decreasing argument of fix." in
+          with Not_found -> user_err Pp.(str "No such fix variable."))
+      | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in
   (id,n, CAst.make ~loc @@ CProdN(bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
@@ -152,7 +152,7 @@ let mkTacCase with_evar = function
   | ic ->
       if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
       then
-	error "Use of numbers as direct arguments of 'case' is not supported.";
+	user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported.");
       TacInductionDestruct (false,with_evar,ic)
 
 let rec mkCLambdaN_simple_loc ?loc bll c =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 75ab1c5ee..a001c6a2b 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -348,7 +348,7 @@ type 'a extra_genarg_printer =
             let bll = List.map (fun (x, _, y) -> x, y) bll in
             if nb >= n then (List.rev (bll@acc)), a
             else strip_ty (bll@acc) (n-nb) a
-        | _ -> error "Cannot translate fix tactic: not enough products" in
+        | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
   let pr_ltac_or_var pr = function
@@ -1089,7 +1089,7 @@ type 'a extra_genarg_printer =
         match ty.CAst.v with
             Glob_term.GProd(na,Explicit,a,b) ->
               strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
-          | _ -> error "Cannot translate fix tactic: not enough products" in
+          | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
   let raw_printers =
@@ -1160,7 +1160,7 @@ type 'a extra_genarg_printer =
         match Term.kind_of_term ty with
             Term.Prod(na,a,b) ->
               strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b
-          | _ -> error "Cannot translate fix tactic: not enough products" in
+          | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
   let pr_atomic_tactic_level env sigma n t =
@@ -1210,7 +1210,7 @@ let declare_extra_genarg_pprule wit
   (h : 'c extra_genarg_printer) =
   begin match wit with
     | ExtraArg s -> ()
-    | _          -> error "Can declare a pretty-printing rule only for extra argument types."
+    | _          -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
   end;
   let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in
   let g x =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e8c9f4eba..51729f4c6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -241,7 +241,7 @@ end) = struct
 	    let liftarg = mkLambda (na, ty, arg) in
 	    let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
 	      if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
-	      else error "build_signature: no constraint can apply on a dependent argument"
+	      else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
 	| _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products")
 	| _, [] ->
 	  (match finalcstr with
@@ -478,7 +478,7 @@ type hypinfo = {
 let get_symmetric_proof b = 
   if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof
 
-let error_no_relation () = error "Cannot find a relation to rewrite."
+let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.")
 
 let rec decompose_app_rel env evd t = 
   (** Head normalize for compatibility with the old meta mechanism *)
@@ -531,7 +531,7 @@ let decompose_applied_relation env sigma (c,l) =
 	let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
 	match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
 	| Some c -> c
-	| None -> error "Cannot find an homogeneous relation to rewrite."
+	| None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.")
 
 let rewrite_db = "rewrite"
 
@@ -837,7 +837,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
 	      sigargs, r.rew_to :: typeargs')
 	  | None ->
 	      if not (Option.is_empty y) then 
-		error "Cannot rewrite inside dependent arguments of a function";
+		user_err Pp.(str "Cannot rewrite inside dependent arguments of a function");
 	      x :: acc, x :: subst, evars, sigargs, x :: typeargs')
       ([], [], evars, sigargs, []) args args'
   in
@@ -1425,7 +1425,7 @@ module Strategies =
 	let unfolded =
 	  try Tacred.try_red_product env sigma c
 	  with e when CErrors.noncritical e ->
-            error "fold: the term is not unfoldable !"
+            user_err Pp.(str "fold: the term is not unfoldable !")
 	in
 	  try
 	    let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
@@ -2204,7 +2204,7 @@ let setoid_symmetry_in id =
   let rec split_last_two = function
     | [c1;c2] -> [],(c1, c2)
     | x::y::z -> let l,res = split_last_two (y::z) in x::l, res
-    | _ -> error "Cannot find an equivalence relation to rewrite."
+    | _ -> user_err Pp.(str "Cannot find an equivalence relation to rewrite.")
   in
   let others,(c1,c2) = split_last_two args in
   let he,c1,c2 =  mkApp (equiv, Array.of_list others),c1,c2 in
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4d7b0f929..75f89a81e 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -60,7 +60,7 @@ let get_tacentry n m =
   else EntryName (rawwit Tacarg.wit_tactic, atactic n)
 
 let get_separator = function
-| None -> error "Missing separator."
+| None -> user_err Pp.(str "Missing separator.")
 | Some sep -> sep
 
 let rec parse_user_entry s sep =
@@ -110,7 +110,7 @@ let get_tactic_entry n =
   else if 1<=n && n<5 then
     Pltac.tactic_expr, Some (Extend.Level (string_of_int n))
   else
-    error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
+    user_err Pp.(str ("Invalid Tactic Notation level: "^(string_of_int n)^"."))
 
 (**********************************************************************)
 (** State of the grammar extensions                                   *)
@@ -170,7 +170,7 @@ let add_tactic_entry (kn, ml, tg) state =
   in
   let () =
     if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
-      error "Notation for simple tactic must start with an identifier."
+      user_err Pp.(str "Notation for simple tactic must start with an identifier.")
   in
   let map = function
   | TacTerm s -> GramTerminal s
@@ -208,7 +208,7 @@ let interp_prod_item = function
     | None ->
       if String.Map.mem s !entry_names then String.Map.find s !entry_names
       else begin match ArgT.name s with
-      | None -> error ("Unknown entry "^s^".")
+      | None -> user_err Pp.(str ("Unknown entry "^s^"."))
       | Some arg -> arg
       end
     | Some n ->
@@ -253,8 +253,8 @@ let pprule pa = {
 
 let check_key key =
   if Tacenv.check_alias key then
-    error "Conflicting tactic notations keys. This can happen when including \
-    twice the same module."
+    user_err Pp.(str "Conflicting tactic notations keys. This can happen when including \
+    twice the same module.")
 
 let cache_tactic_notation (_, tobj) =
   let key = tobj.tacobj_key in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 6c7eb8c89..e431a13bc 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -252,7 +252,7 @@ and intern_or_and_intro_pattern lf ist = function
 let intern_or_and_intro_pattern_loc lf ist = function
   | ArgVar (_,id) as x ->
       if find_var id ist then x
-      else error "Disjunctive/conjunctive introduction pattern expected."
+      else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.")
   | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l)
 
 let intern_intro_pattern_naming_loc lf ist (loc,pat) =