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

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 0a68ff129..e6278943d 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
@@ -1886,7 +1886,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 617d3d701..7e8cb4e63 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 ->