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

13 files changed, 34 insertions, 34 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index edcfa99c86..2cb837ba03 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -220,9 +220,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
       | PSoApp (n,args),m ->
         let fold (ans, seen) = function
         | PRel n ->
-          let () = if Int.Set.mem n seen then error "Non linear second-order pattern" in
+          let () = if Int.Set.mem n seen then user_err (str "Non linear second-order pattern") in
           (n :: ans, Int.Set.add n seen)
-        | _ -> error "Only bound indices allowed in second order pattern matching."
+        | _ -> user_err (str "Only bound indices allowed in second order pattern matching.")
         in
         let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in
         let frels = free_rels sigma cT in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 42aaf3a227..b944da7500 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1051,7 +1051,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c ->
       begin match occs with
       | Some _ ->
-        error "Cannot force abstraction on identity instance."
+        user_err Pp.(str "Cannot force abstraction on identity instance.")
       | None ->
         make_subst (ctxt',l,occsl)
       end
@@ -1070,7 +1070,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
       let set_var k =
         match occs with
         | Some Locus.AllOccurrences -> mkVar id
-        | Some _ -> error "Selection of specific occurrences not supported"
+        | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported")
         | None ->
         let evty = set_holes evdref cty subst in
         let instance = Filter.filter_list filter instance in
@@ -1108,10 +1108,10 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
               (* This is an arbitrary choice *)
               let evd = Evd.define evk (Constr.mkVar id) evd in
               match evar_conv_x ts env_evar evd CUMUL idty evty with
-              | UnifFailure _ -> error "Cannot find an instance"
+              | UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
               | Success evd ->
               match reconsider_unif_constraints (evar_conv_x ts) evd with
-              | UnifFailure _ -> error "Cannot find an instance"
+              | UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
               | Success evd ->
               evd
             else
@@ -1245,7 +1245,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
   | None -> evd
   | Some (evk,ev_info,l) ->
       let rec aux = function
-      | [] -> error "Unsolvable existential variables."
+      | [] -> user_err Pp.(str "Unsolvable existential variables.")
       | a::l ->
           try
             let conv_algo = evar_conv_x ts in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4ada91eb59..98e71c7fd9 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1050,7 +1050,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
   | None -> None,candidates
   | Some filter -> restrict_hyps evd evk filter candidates in
   match candidates,filter with
-  | UpdateWith [], _ -> error "Not solvable."
+  | UpdateWith [], _ -> user_err Pp.(str "Not solvable.")
   | UpdateWith [nc],_ ->
       let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in
       raise (EvarSolvedWhileRestricting (evd,mkEvar ev))
@@ -1230,7 +1230,7 @@ let check_evar_instance evd evk1 body conv_algo =
   (* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
   let ty =
     try Retyping.get_type_of ~lax:true evenv evd body
-    with Retyping.RetypeError _ -> error "Ill-typed evar instance"
+    with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance")
   in
   match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with
   | Success evd -> evd
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 429e5005ec..7f3bafc685 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -97,7 +97,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
   and ntypes = mib.mind_ntypes
   and nconstr = Array.length mip.mind_consnames in
   let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in
-  if j > nconstr then error "Not enough constructors in the type.";
+  if j > nconstr then user_err Pp.(str "Not enough constructors in the type.");
     substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1))
 
 (* Number of constructors *)
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index e4fbf8d542..211ffbe01e 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -50,9 +50,9 @@ let is_nowhere = function
 
 let simple_clause_of enum_hyps cl =
   let error_occurrences () =
-    CErrors.error "This tactic does not support occurrences selection" in
+    CErrors.user_err Pp.(str "This tactic does not support occurrences selection") in
   let error_body_selection () =
-    CErrors.error "This tactic does not support body selection" in
+    CErrors.user_err Pp.(str "This tactic does not support body selection") in
   let hyps =
     match cl.onhyps with
     | None ->
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 0228f63cdc..afaa20b6f6 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -383,7 +383,7 @@ let native_norm env sigma c ty =
   let c = EConstr.Unsafe.to_constr c in
   let ty = EConstr.Unsafe.to_constr ty in
   if Coq_config.no_native_compiler then
-    error "Native_compute reduction has been disabled at configure time."
+    user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
   else
   let penv = Environ.pre_env env in
   (*
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index a8012d35f8..1c8ad0cddd 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -230,7 +230,7 @@ let instantiate_pattern env sigma lvar c =
 	  error_instantiate_pattern id (List.subtract Id.equal ctx vars)
        with Not_found (* Map.find failed *) ->
 	 x)
-  | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
+  | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.")
   | c ->
       map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
   aux [] c
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index 7d65925e57..8e190f40b9 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -20,13 +20,13 @@ let make_red_flag l =
     | FZeta :: lf -> add_flag { red with rZeta = true } lf
     | FConst l :: lf ->
 	if red.rDelta then
-	  CErrors.error
-	    "Cannot set both constants to unfold and constants not to unfold";
+	  CErrors.user_err Pp.(str
+	    "Cannot set both constants to unfold and constants not to unfold");
         add_flag { red with rConst = union_consts red.rConst l } lf
     | FDeltaBut l :: lf ->
 	if red.rConst <> [] && not red.rDelta then
-	  CErrors.error
-	    "Cannot set both constants to unfold and constants not to unfold";
+	  CErrors.user_err Pp.(str
+	    "Cannot set both constants to unfold and constants not to unfold");
         add_flag
           { red with rConst = union_consts red.rConst l; rDelta = true }
           lf
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 117ed338ee..e7c9635829 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1219,7 +1219,7 @@ let clos_norm_flags flgs env sigma t =
     EConstr.of_constr (CClosure.norm_val
       (CClosure.create_clos_infos ~evars flgs env)
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
-  with e when is_anomaly e -> error "Tried to normalize ill-typed term"
+  with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
 
 let clos_whd_flags flgs env sigma t =
   try
@@ -1227,7 +1227,7 @@ let clos_whd_flags flgs env sigma t =
     EConstr.of_constr (CClosure.whd_val
       (CClosure.create_clos_infos ~evars flgs env)
       (CClosure.inject (EConstr.Unsafe.to_constr t)))
-  with e when is_anomaly e -> error "Tried to normalize ill-typed term"
+  with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
 
 let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
 let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ())
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 67221046bd..3d41d2ddd5 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
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 919e95a8ee..d7b4842810 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -422,7 +422,7 @@ let add_class cl =
 	     match inst with
 	     | Some (Backward, info) ->
 	       (match body with
-	       | None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
+	       | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
 	       | Some b -> declare_instance (Some info) false (ConstRef b))
 	     | _ -> ())
   cl.cl_projs
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index cac6c50572..d1643a8c7d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1250,7 +1250,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
       | Prod (_,c1,c2) ->
         let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
 	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
-      | _ -> error "Apply_Head_Then"
+      | _ -> user_err Pp.(str "Apply_Head_Then")
   in
     apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd
 
@@ -1516,7 +1516,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 =
 let iter_fail f a =
   let n = Array.length a in
   let rec ffail i =
-    if Int.equal i n then error "iter_fail"
+    if Int.equal i n then user_err Pp.(str "iter_fail")
     else
       try f a.(i)
       with ex when precatchable_exception ex -> ffail (i+1)
@@ -1754,8 +1754,8 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
 	   w_typed_unify_array env evd flags f1 l1 f2 l2,cl
 	 else w_typed_unify env evd CONV flags op cl,cl
        with ex when Pretype_errors.unsatisfiable_exception ex ->
-	    bestexn := Some ex; error "Unsat")
-       else error "Bound 1"
+	    bestexn := Some ex; user_err Pp.(str "Unsat"))
+       else user_err Pp.(str "Bound 1")
      with ex when precatchable_exception ex ->
        (match EConstr.kind evd cl with
 	  | App (f,args) ->
@@ -1804,7 +1804,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
 	       with ex when precatchable_exception ex ->
 		 matchrec c)
 
-          | _ -> error "Match_subterm"))
+          | _ -> user_err Pp.(str "Match_subterm")))
   in
   try matchrec cl
   with ex when precatchable_exception ex ->
@@ -1820,7 +1820,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
     let (evd,c as a) = a () in
       if List.exists (fun (evd',c') -> EConstr.eq_constr evd' c c') b then b else a :: b
   in
-  let fail str _ = error str in
+  let fail str _ = user_err (Pp.str str) in
   let bind f g a =
     let a1 = try f a
              with ex
@@ -1956,7 +1956,7 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
     | _, Meta p2 ->
         (* Find the predicate *)
         secondOrderAbstractionAlgo dep env evd flags ty1 (p2, oplist2)
-    | _ -> error "w_unify2"
+    | _ -> user_err Pp.(str "w_unify2")
 
 (* The unique unification algorithm works like this: If the pattern is
    flexible, and the goal has a lambda-abstraction at the head, then
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 74998349be..b08666483e 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -355,7 +355,7 @@ and nf_cofix env sigma cf =
 
 let cbv_vm env sigma c t  =
   if Termops.occur_meta_or_existential sigma c then
-    CErrors.error "vm_compute does not support existential variables.";
+    CErrors.user_err Pp.(str "vm_compute does not support existential variables.");
   (** This evar-normalizes terms beforehand *)
   let c = EConstr.to_constr sigma c in
   let t = EConstr.to_constr sigma t in