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

6 files changed, 25 insertions, 25 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 9e0a2a03eb..33a86402ef 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -163,7 +163,7 @@ let error_incompatible_inst clenv mv  =
 let clenv_assign mv rhs clenv =
   let rhs_fls = mk_freelisted rhs in
   if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then
-    error "clenv_assign: circularity in unification";
+    user_err Pp.(str "clenv_assign: circularity in unification");
   try
     if meta_defined clenv.evd mv then
       if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then
@@ -174,7 +174,7 @@ let clenv_assign mv rhs clenv =
       let st = (Conv,TypeNotProcessed) in
       {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
   with Not_found ->
-    error "clenv_assign: undefined meta"
+    user_err Pp.(str "clenv_assign: undefined meta")
 
 
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index b9c9257969..b1fe128a24 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -39,11 +39,11 @@ let define_and_solve_constraints evk c env evd =
       pbs
   with
     | Success evd -> evd
-    | UnifFailure _ -> error "Instance does not satisfy the constraints."
+    | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.")
 
 let w_refine (evk,evi) (ltac_var,rawc) sigma =
   if Evd.is_defined sigma evk then
-    error "Instantiate called on already-defined evar";
+    user_err Pp.(str "Instantiate called on already-defined evar");
   let env = Evd.evar_filtered_env evi in
   let sigma',typed_c =
     let flags = {
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 54345abd97..cd2cfbd32f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -141,7 +141,7 @@ let occur_vars_in_decl env sigma hyps d =
 let reorder_context env sigma sign ord =
   let ords = List.fold_right Id.Set.add ord Id.Set.empty in
   if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then
-    error "Order list has duplicates";
+    user_err Pp.(str "Order list has duplicates");
   let rec step ord expected ctxt_head moved_hyps ctxt_tail =
     match ord with
       | [] -> List.rev ctxt_tail @ ctxt_head
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 92b4e788a2..aaceb7b762 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -71,7 +71,7 @@ let get_universe_binders () =
 
 exception NoSuchGoal
 let _ = CErrors.register_handler begin function
-  | NoSuchGoal -> CErrors.error "No such goal."
+  | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
   | _ -> raise CErrors.Unhandled
 end
 let get_nth_V82_goal i =
@@ -87,12 +87,12 @@ let get_goal_context_gen i =
 
 let get_goal_context i =
   try get_goal_context_gen i
-  with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
-     | NoSuchGoal -> CErrors.error "No such goal."
+  with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
+     | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
 
 let get_current_goal_context () =
   try get_goal_context_gen 1
-  with Proof_global.NoCurrentProof -> CErrors.error "No focused proof."
+  with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
      | NoSuchGoal -> 
     (* spiwack: returning empty evar_map, since if there is no goal, under focus,
         there is no accessible evar either *)
@@ -143,7 +143,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
     in
     (p,status)
   with
-    Proof_global.NoCurrentProof -> CErrors.error "No focused proof"
+    Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof")
 
 let by tac = Proof_global.with_current_proof (fun _ -> solve (Vernacexpr.SelectNth 1) None tac)
 
diff --git a/proofs/proof.ml b/proofs/proof.ml
index b2103489a7..2aa620c1da 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -66,14 +66,14 @@ exception FullyUnfocused
 
 let _ = CErrors.register_handler begin function
   | CannotUnfocusThisWay ->
-    CErrors.error "This proof is focused, but cannot be unfocused this way"
+    CErrors.user_err Pp.(str "This proof is focused, but cannot be unfocused this way")
   | NoSuchGoals (i,j) when Int.equal i j ->
       CErrors.user_err ~hdr:"Focus" Pp.(str"No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
       CErrors.user_err ~hdr:"Focus" Pp.(
         str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
       )
-  | FullyUnfocused -> CErrors.error "The proof is not focused"
+  | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
   | _ -> raise CErrors.Unhandled
 end
 
@@ -301,10 +301,10 @@ exception HasShelvedGoals
 exception HasGivenUpGoals
 exception HasUnresolvedEvar
 let _ = CErrors.register_handler begin function
-  | UnfinishedProof -> CErrors.error "Some goals have not been solved."
-  | HasShelvedGoals -> CErrors.error "Some goals have been left on the shelf."
-  | HasGivenUpGoals -> CErrors.error "Some goals have been given up."
-  | HasUnresolvedEvar -> CErrors.error "Some existential variables are uninstantiated."
+  | UnfinishedProof -> CErrors.user_err Pp.(str "Some goals have not been solved.")
+  | HasShelvedGoals -> CErrors.user_err Pp.(str "Some goals have been left on the shelf.")
+  | HasGivenUpGoals -> CErrors.user_err Pp.(str "Some goals have been given up.")
+  | HasUnresolvedEvar -> CErrors.user_err Pp.(str "Some existential variables are uninstantiated.")
   | _ -> raise CErrors.Unhandled
 end
 
@@ -420,9 +420,9 @@ module V82 = struct
         let evl = Evarutil.non_instantiated sigma in
         let evl = Evar.Map.bindings evl in
         if (n <= 0) then
-          CErrors.error "incorrect existential variable index"
+          CErrors.user_err Pp.(str "incorrect existential variable index")
         else if CList.length evl < n then
-          CErrors.error "not so many uninstantiated existential variables"
+          CErrors.user_err Pp.(str "not so many uninstantiated existential variables")
         else
           CList.nth evl (n-1)
       in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 95aee72cb5..4d2f534a76 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -36,7 +36,7 @@ let proof_modes = Hashtbl.create 6
 let find_proof_mode n =
   try Hashtbl.find proof_modes n
   with Not_found ->
-    CErrors.error (Format.sprintf "No proof mode named \"%s\"." n)
+    CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n))
 
 let register_proof_mode ({name = n} as m) =
   Hashtbl.add proof_modes n (CEphemeron.create m)
@@ -124,13 +124,13 @@ let push a l = l := a::!l;
 
 exception NoSuchProof
 let _ = CErrors.register_handler begin function
-  | NoSuchProof -> CErrors.error "No such proof."
+  | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.")
   | _ -> raise CErrors.Unhandled
 end
 
 exception NoCurrentProof
 let _ = CErrors.register_handler begin function
-  | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)."
+  | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
   | _ -> raise CErrors.Unhandled
 end
 
@@ -299,7 +299,7 @@ let set_used_variables l =
   | [] -> raise NoCurrentProof
   | p :: rest ->
       if not (Option.is_empty p.section_vars) then
-        CErrors.error "Used section variables can be declared only once";
+        CErrors.user_err Pp.(str "Used section variables can be declared only once");
       pstates := { p with section_vars = Some ctx} :: rest;
       ctx, to_clear
 
@@ -637,7 +637,7 @@ module Bullet = struct
 	current_behavior :=
           try Hashtbl.find behaviors n
           with Not_found ->
-            CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
+            CErrors.user_err Pp.(str ("Unknown bullet behavior: \"" ^ n ^ "\"."))
       end
     })
 
@@ -687,9 +687,9 @@ let parse_goal_selector = function
       let err_msg = "The default selector must be \"all\" or a natural number." in
       begin try
               let i = int_of_string i in
-              if i < 0 then CErrors.error err_msg;
+              if i < 0 then CErrors.user_err Pp.(str err_msg);
               Vernacexpr.SelectNth i
-        with Failure _ -> CErrors.error err_msg
+        with Failure _ -> CErrors.user_err Pp.(str err_msg)
       end
 
 let _ =