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

9 files changed, 40 insertions, 37 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 918371d55..46d66b9d0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -938,7 +938,7 @@ module V85 = struct
     | Some (evd', fk) ->
        if unique then
          (match get_result (fk NotApplicable) with
-          | Some (evd'', fk') -> error "Typeclass resolution gives multiple solutions"
+          | Some (evd'', fk') -> user_err Pp.(str "Typeclass resolution gives multiple solutions")
           | None -> evd')
        else evd'
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index e87368dec..986f53139 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -62,7 +62,7 @@ let registered_e_assumption =
 
 let first_goal gls =
   let gl = gls.Evd.it and sig_0 = gls.Evd.sigma in
-  if List.is_empty gl then error "first_goal";
+  if List.is_empty gl then user_err Pp.(str "first_goal");
   { Evd.it = List.hd gl; Evd.sigma = sig_0; }
 
 (* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
@@ -73,7 +73,7 @@ let apply_tac_list tac glls =
   | (g1::rest) ->
       let gl = apply_sig_tac sigr tac g1 in
       repackage sigr (gl@rest)
-  | _ -> error "apply_tac_list"
+  | _ -> user_err Pp.(str "apply_tac_list")
 
 let one_step l gl =
   [Proofview.V82.of_tactic Tactics.intro]
@@ -82,7 +82,7 @@ let one_step l gl =
   @ (List.map (fun c -> Proofview.V82.of_tactic (assumption c)) (pf_ids_of_hyps gl))
 
 let rec prolog l n gl =
-  if n <= 0 then error "prolog - failure";
+  if n <= 0 then user_err Pp.(str "prolog - failure");
   let prol = (prolog l (n-1)) in
   (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
 
@@ -402,7 +402,7 @@ let e_search_auto debug (in_depth,p) lems db_list gl =
     s.tacres
   with Not_found ->
     pr_info_nop d;
-    error "eauto: search failed"
+    user_err Pp.(str "eauto: search failed")
 
 (* let e_search_auto_key = Profile.declare_profile "e_search_auto" *)
 (* let e_search_auto = Profile.profile5 e_search_auto_key e_search_auto *)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index d023b4568..bcd31cb7e 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -103,7 +103,7 @@ let get_coq_eq ctx =
       (Universes.fresh_inductive_instance (Global.env ()) eq) in
       mkIndU eq, mkConstructUi (eq,1), ctx
   with Not_found ->
-    error "eq not found."
+    user_err Pp.(str "eq not found.")
 
 let univ_of_eq env eq =
   let eq = EConstr.of_constr eq in
@@ -120,6 +120,8 @@ let univ_of_eq env eq =
 (* in which case, a symmetry lemma is definable                       *)
 (**********************************************************************)
 
+let error msg = user_err Pp.(str msg)
+
 let get_sym_eq_data env (ind,u) =
   let (mib,mip as specif) = lookup_mind_specif env ind in
   if not (Int.equal (Array.length mib.mind_packets) 1) ||
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 70d6fe90c..839ec4ce1 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -164,7 +164,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
   let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
   let (equiv, args) = decompose_app_vect sigma (Clenv.clenv_type eqclause) in
   let arglen = Array.length args in
-  let () = if arglen < 2 then error "The term provided is not an applied relation." in
+  let () = if arglen < 2 then user_err Pp.(str "The term provided is not an applied relation.") in
   let c1 = args.(arglen - 2) in
   let c2 = args.(arglen - 1) in
   let try_occ (evd', c') =
@@ -441,7 +441,7 @@ let adjust_rewriting_direction args lft2rgt =
     (* equality to a constant, like in eq_true *)
     (* more natural to see -> as the rewriting to the constant *)
     if not lft2rgt then
-      error "Rewriting non-symmetric equality not allowed from right-to-left.";
+      user_err Pp.(str "Rewriting non-symmetric equality not allowed from right-to-left.");
     None
   | _ ->
     (* other equality *)
@@ -865,7 +865,7 @@ let descend_then env sigma head dirn =
   let IndType (indf,_) =
     try find_rectype env sigma (get_type_of env sigma head)
     with Not_found ->
-      error "Cannot project on an inductive type derived from a dependency." in
+      user_err Pp.(str "Cannot project on an inductive type derived from a dependency.") in
   let indp,_ = (dest_ind_family indf) in
   let ind, _ = check_privacy env indp in
   let (mib,mip) = lookup_mind_specif env ind in
@@ -1202,7 +1202,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
           evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
 	dflt
       with Evarconv.UnableToUnify _ ->
-	error "Cannot solve a unification problem."
+	user_err Pp.(str "Cannot solve a unification problem.")
     else
       let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
 	| (_sigS,[a;p]) -> (a, p)
@@ -1219,7 +1219,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
 	      let exist_term = EConstr.of_constr exist_term in
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
-              error "Cannot solve a unification problem."
+              user_err Pp.(str "Cannot solve a unification problem.")
 	| None ->
             (* This at least happens if what has been detected as a
                dependency is not one; use an evasive error message;
@@ -1227,7 +1227,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
                tried in the first place in make_iterated_tuple instead
                of approximatively computing the free rels; then
                unsolved evars would mean not binding rel *)
-	    error "Cannot solve a unification problem."
+	    user_err Pp.(str "Cannot solve a unification problem.")
   in
   let scf = sigrec_clausal_form siglen ty in
     !evdref, Evarutil.nf_evar !evdref scf
@@ -1887,7 +1887,7 @@ let cond_eq_term c t gl =
 
 let rewrite_assumption_cond cond_eq_term cl =
   let rec arec hyps gl = match hyps with
-    | [] -> error "No such assumption."
+    | [] -> user_err Pp.(str "No such assumption.")
     | hyp ::rest ->
         let id = NamedDecl.get_id hyp in
 	begin
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e6edae7ef..48a7b3f75 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -59,7 +59,7 @@ let head_constr_bound sigma t =
   | _ -> raise Bound
 
 let head_constr sigma c =
-  try head_constr_bound sigma c with Bound -> error "Bound head variable."
+  try head_constr_bound sigma c with Bound -> user_err Pp.(str "Bound head variable.")
 
 let decompose_app_bound sigma t =
   let t = strip_outer_cast sigma t in
@@ -167,7 +167,7 @@ let write_warn_hint = function
 | "Lax" -> warn_hint := `LAX
 | "Warn" -> warn_hint := `WARN
 | "Strict" -> warn_hint := `STRICT
-| _ -> error "Only the following flags are accepted: Lax, Warn, Strict."
+| _ -> user_err Pp.(str "Only the following flags are accepted: Lax, Warn, Strict.")
 
 let _ =
   Goptions.declare_string_option
@@ -767,7 +767,7 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with
 
 let try_head_pattern c =
   try head_pattern_bound c
-  with BoundPattern -> error "Bound head variable."
+  with BoundPattern -> user_err Pp.(str "Bound head variable.")
 
 let with_uid c = { obj = c; uid = fresh_key () }
 
@@ -980,8 +980,8 @@ let get_db dbname =
 let add_hint dbname hintlist =
   let check (_, h) =
     let () = if KNmap.mem h.code.uid !statustable then
-      error "Conflicting hint keys. This can happen when including \
-      twice the same module."
+      user_err Pp.(str "Conflicting hint keys. This can happen when including \
+      twice the same module.")
     in
     statustable := KNmap.add h.code.uid false !statustable
   in
@@ -1246,10 +1246,10 @@ let prepare_hint check (poly,local) env init (sigma,c) =
       let t = Evarutil.nf_evar sigma (existential_type sigma ev) in
       let t = List.fold_right (fun (e,id) c -> replace_term sigma e id c) !subst t in
       if not (closed0 sigma c) then
-	error "Hints with holes dependent on a bound variable not supported.";
+	user_err Pp.(str "Hints with holes dependent on a bound variable not supported.");
       if occur_existential sigma t then
 	(* Not clever enough to construct dependency graph of evars *)
-	error "Not clever enough to deal with evars dependent in other evars.";
+	user_err Pp.(str "Not clever enough to deal with evars dependent in other evars.");
       raise (Found (c,t))
     | _ -> EConstr.iter sigma find_next_evar c in
   let rec iter c =
@@ -1322,7 +1322,7 @@ let interp_hints poly =
 
 let add_hints local dbnames0 h =
   if String.List.mem "nocore" dbnames0 then
-    error "The hint database \"nocore\" is meant to stay empty.";
+    user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
   let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
   let env = Global.env() in
   let sigma = Evd.from_env env in
@@ -1471,7 +1471,7 @@ let pr_applicable_hint () =
   let pts = get_pftreestate () in
   let glss = Proof.V82.subgoals pts in
   match glss.Evd.it with
-  | [] -> CErrors.error "No focused goal."
+  | [] -> CErrors.user_err Pp.(str "No focused goal.")
   | g::_ ->
     pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index dce98eed7..fd5eabe64 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -460,7 +460,7 @@ let find_this_eq_data_decompose gl eqn =
   let eq_args =
     try extract_eq_args gl eq_args
     with PatternMatchingFailure ->
-      error "Don't know what to do with JMeq on arguments not of same type." in
+      user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in
   (lbeq,u,eq_args)
 
 let match_eq_nf gls eqn (ref, hetero) =
@@ -477,7 +477,7 @@ let dest_nf_eq gls eqn =
   try
     snd (first_match (match_eq_nf gls eqn) equalities)
   with PatternMatchingFailure ->
-    error "Not an equality."
+    user_err Pp.(str "Not an equality.")
 
 (*** Sigma-types *)
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5c4b73a62..b951e7ceb 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -292,27 +292,27 @@ let error_too_many_names pats =
 
 let get_names (allow_conj,issimple) (loc, pat as x) = match pat with
   | IntroNaming IntroAnonymous | IntroForthcoming _ ->
-      error "Anonymous pattern not allowed for inversion equations."
+      user_err Pp.(str "Anonymous pattern not allowed for inversion equations.")
   | IntroNaming (IntroFresh _) ->
-      error "Fresh pattern not allowed for inversion equations."
+      user_err Pp.(str "Fresh pattern not allowed for inversion equations.")
   | IntroAction IntroWildcard ->
-      error "Discarding pattern not allowed for inversion equations."
+      user_err Pp.(str "Discarding pattern not allowed for inversion equations.")
   | IntroAction (IntroRewrite _) ->
-      error "Rewriting pattern not allowed for inversion equations."
+      user_err Pp.(str "Rewriting pattern not allowed for inversion equations.")
   | IntroAction (IntroOrAndPattern (IntroAndPattern [])) when allow_conj -> (None, [])
   | IntroAction (IntroOrAndPattern (IntroAndPattern ((_,IntroNaming (IntroIdentifier id)) :: _ as l) | IntroOrPattern [(_,IntroNaming (IntroIdentifier id)) :: _ as l ]))
       when allow_conj -> (Some id,l)
   | IntroAction (IntroOrAndPattern (IntroAndPattern _)) ->
       if issimple then
-        error"Conjunctive patterns not allowed for simple inversion equations."
+        user_err Pp.(str"Conjunctive patterns not allowed for simple inversion equations.")
       else
-        error"Nested conjunctive patterns not allowed for inversion equations."
+        user_err Pp.(str"Nested conjunctive patterns not allowed for inversion equations.")
   | IntroAction (IntroInjection l) ->
-      error "Injection patterns not allowed for inversion equations."
+      user_err Pp.(str "Injection patterns not allowed for inversion equations.")
   | IntroAction (IntroOrAndPattern (IntroOrPattern _)) ->
-      error "Disjunctive patterns not allowed for inversion equations."
+      user_err Pp.(str "Disjunctive patterns not allowed for inversion equations.")
   | IntroAction (IntroApplyOn (c,pat)) ->
-      error "Apply patterns not allowed for inversion equations."
+      user_err Pp.(str "Apply patterns not allowed for inversion equations.")
   | IntroNaming (IntroIdentifier id) ->
       (Some id,[x])
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index fe9cb123c..c495b5ece 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -69,7 +69,7 @@ let tclTHENSEQ       = tclTHENLIST
 
 let nthDecl m gl =
   try List.nth (pf_hyps gl) (m-1)
-  with Failure _ -> error "No such assumption."
+  with Failure _ -> user_err Pp.(str "No such assumption.")
 
 let nthHypId m gl = nthDecl m gl |> NamedDecl.get_id
 let nthHyp m gl   = mkVar (nthHypId m gl)
@@ -80,7 +80,7 @@ let lastHyp gl    = nthHyp 1 gl
 
 let nLastDecls n gl =
   try List.firstn n (pf_hyps gl)
-  with Failure _ -> error "Not enough hypotheses in the goal."
+  with Failure _ -> user_err Pp.(str "Not enough hypotheses in the goal.")
 
 let nLastHypsId n gl = List.map (NamedDecl.get_id) (nLastDecls n gl)
 let nLastHyps n gl   = List.map mkVar (nLastHypsId n gl)
@@ -533,11 +533,11 @@ module New = struct
     let hyps = Proofview.Goal.hyps gl in
     try
       List.nth hyps (m-1)
-    with Failure _ -> CErrors.error "No such assumption."
+    with Failure _ -> CErrors.user_err Pp.(str "No such assumption.")
 
   let nLastDecls gl n =
     try List.firstn n (Proofview.Goal.hyps gl)
-    with Failure _ -> error "Not enough hypotheses in the goal."
+    with Failure _ -> CErrors.user_err Pp.(str "Not enough hypotheses in the goal.")
 
   let nthHypId m gl =
     (** We only use [id] *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c713a31fa..c7847e412 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -195,6 +195,7 @@ let introduction ?(check=true) id =
   end }
 
 let refine          = Tacmach.refine
+let error msg = CErrors.user_err Pp.(str msg)
 
 let convert_concl ?(check=true) ty k =
   Proofview.Goal.enter { enter = begin fun gl ->