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

1 files changed, 39 insertions, 39 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a08c79c40..6c1d64cfe 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -139,7 +139,7 @@ let make_cases s =
 let show_match id =
   let patterns =
     try make_cases_aux (Nametab.global id)
-    with Not_found -> error "Unknown inductive type."
+    with Not_found -> user_err Pp.(str "Unknown inductive type.")
   in
   let pr_branch l =
     str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>"
@@ -305,7 +305,7 @@ let print_strategy r =
     let key = match r with
     | VarRef id -> VarKey id
     | ConstRef cst -> ConstKey cst
-    | IndRef _ | ConstructRef _ -> error "The reference is not unfoldable"
+    | IndRef _ | ConstructRef _ -> user_err Pp.(str "The reference is not unfoldable")
     in
     let lvl = get_strategy oracle key in
     Feedback.msg_notice (pr_strategy (r, lvl))
@@ -451,8 +451,8 @@ let start_proof_and_print k l hook =
                                    concl (Tacticals.New.tclCOMPLETE tac)
           in Evd.set_universe_context sigma ctx, EConstr.of_constr c
         with Logic_monad.TacticFailure e when Logic.catchable_exception e ->
-          error "The statement obligations could not be resolved \
-                 automatically, write a statement definition first."
+          user_err Pp.(str "The statement obligations could not be resolved \
+                 automatically, write a statement definition first.")
       in Some hook
     else None
   in
@@ -551,9 +551,9 @@ let vernac_inductive poly lo finite indl =
       indl;
   match indl with
   | [ ( _ , _ , _ ,(Record|Structure), Constructors _ ),_ ] ->
-      CErrors.error "The Record keyword is for types defined using the syntax { ... }."
+      user_err Pp.(str "The Record keyword is for types defined using the syntax { ... }.")
   | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
-      CErrors.error "The Variant keyword does not support syntax { ... }."
+      user_err Pp.(str "The Variant keyword does not support syntax { ... }.")
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
       vernac_record (match b with Class _ -> Class false | _ -> b)
        poly finite id bl c oc fs
@@ -564,16 +564,16 @@ let vernac_inductive poly lo finite indl =
   	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
       in vernac_record (Class true) poly finite id bl c None [f]
   | [ ( _ , _, _, Class _, Constructors _), [] ] ->
-      CErrors.error "Inductive classes not supported"
+      user_err Pp.(str "Inductive classes not supported")
   | [ ( id , bl , c , Class _, _), _ :: _ ] ->
-      CErrors.error "where clause not supported for classes"
+      user_err Pp.(str "where clause not supported for classes")
   | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] ->
-      CErrors.error "where clause not supported for (co)inductive records"
+      user_err Pp.(str "where clause not supported for (co)inductive records")
   | _ -> let unpack = function
       | ( (false, id) , bl , c , _ , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
       | ( (true,_),_,_,_,Constructors _),_ ->
-          CErrors.error "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead."
-      | _ -> CErrors.error "Cannot handle mutually (co)inductive records."
+          user_err Pp.(str "Variant types do not handle the \"> Name\" syntax, which is reserved for records. Use the \":>\" syntax on constructors instead.")
+      | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
     in
     let indl = List.map unpack indl in
     do_mutual_inductive indl poly lo finite
@@ -631,11 +631,11 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
-    error "Modules and Module Types are not allowed inside sections.";
+    user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
   let binders_ast = List.map
    (fun (export,idl,ty) ->
      if not (Option.is_empty export) then
-      error "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument."
+      user_err Pp.(str "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
      else (idl,ty)) binders_ast in
   let mp =
     Declaremods.declare_module Modintern.interp_module_ast
@@ -649,7 +649,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
-    error "Modules and Module Types are not allowed inside sections.";
+    user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
   match mexpr_ast_l with
     | [] ->
        check_no_pending_proofs ();
@@ -674,7 +674,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        let binders_ast = List.map
         (fun (export,idl,ty) ->
           if not (Option.is_empty export) then
-           error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument."
+           user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
           else (idl,ty)) binders_ast in
        let mp =
          Declaremods.declare_module Modintern.interp_module_ast
@@ -694,7 +694,7 @@ let vernac_end_module export (loc,id as lid) =
 
 let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
   if Lib.sections_are_opened () then
-    error "Modules and Module Types are not allowed inside sections.";
+    user_err Pp.(str "Modules and Module Types are not allowed inside sections.");
 
   match mty_ast_l with
     | [] ->
@@ -722,7 +722,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 	let binders_ast = List.map
           (fun (export,idl,ty) ->
             if not (Option.is_empty export) then
-              error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument."
+              user_err Pp.(str "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument.")
             else (idl,ty)) binders_ast in
 	let mp =
           Declaremods.declare_modtype Modintern.interp_module_ast
@@ -846,7 +846,7 @@ let vernac_set_end_tac tac =
   let env = Genintern.empty_glob_sign (Global.env ()) in
   let _, tac = Genintern.generic_intern env tac in
   if not (refining ()) then
-    error "Unknown command of the non proof-editing mode.";
+    user_err Pp.(str "Unknown command of the non proof-editing mode.");
   set_end_tac tac
     (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
 
@@ -903,7 +903,7 @@ let vernac_chdir = function
 	  (* Cd is typically used to control the output directory of
 	  extraction. A failed Cd could lead to overwriting .ml files
 	  so we make it an error. *)
-	  CErrors.error ("Cd failed: " ^ err)
+	  user_err Pp.(str ("Cd failed: " ^ err))
       end;
       if_verbose Feedback.msg_info (str (Sys.getcwd()))
 
@@ -972,7 +972,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   let never_unfold_flag = List.mem `ReductionNeverUnfold flags in
 
   let err_incompat x y =
-    error ("Options \""^x^"\" and \""^y^"\" are incompatible.") in
+    user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in
 
   if assert_flag && rename_flag then
     err_incompat "assert" "rename";
@@ -1018,7 +1018,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
     | { name = Anonymous; notation_scope = Some _ } :: args ->
        check_extra_args args
     | _ ->
-       error "Extra notation scopes can be set on anonymous and explicit arguments only."
+       user_err Pp.(str "Extra notation scopes can be set on anonymous and explicit arguments only.")
   in
 
   let args, scopes =
@@ -1032,12 +1032,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   in
 
   if Option.cata (fun n -> n > num_args) false nargs_for_red then
-    error "The \"/\" modifier should be put before any extra scope.";
+    user_err Pp.(str "The \"/\" modifier should be put before any extra scope.");
 
   let scopes_specified = List.exists Option.has_some scopes in
   
   if scopes_specified && clear_scopes_flag then
-    error "The \"clear scopes\" flag is incompatible with scope annotations.";
+    user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations.");
 
   let names = List.map (fun { name } -> name) args in
   let names = names :: List.map (List.map fst) more_implicits in
@@ -1062,7 +1062,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
     | name1 :: names1, name2 :: names2 ->
        if Name.equal name1 name2 then
          name1 :: names_union names1 names2
-       else error "Argument lists should agree on the names they provide."
+       else user_err Pp.(str "Argument lists should agree on the names they provide.")
   in
 
   let names = List.fold_left names_union [] names in
@@ -1143,10 +1143,10 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   let implicits_specified = match implicits with [[]] -> false | _ -> true in
 
   if implicits_specified && clear_implicits_flag then
-    error "The \"clear implicits\" flag is incompatible with implicit annotations";
+    user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations");
 
   if implicits_specified && default_implicits_flag then
-    error "The \"default implicits\" flag is incompatible with implicit annotations";
+    user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations");
 
   let rargs =
     Util.List.map_filter (function (n, true) -> Some n | _ -> None)
@@ -1452,8 +1452,8 @@ let vernac_set_strategy locality l =
     match smart_global r with
       | ConstRef sp -> EvalConstRef sp
       | VarRef id -> EvalVarRef id
-      | _ -> error
-          "cannot set an inductive type or a constructor as transparent" in
+      | _ -> user_err Pp.(str
+          "cannot set an inductive type or a constructor as transparent") in
   let l = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) l in
   Redexpr.set_strategy local l
 
@@ -1463,8 +1463,8 @@ let vernac_set_opacity locality (v,l) =
     match smart_global r with
       | ConstRef sp -> EvalConstRef sp
       | VarRef id -> EvalVarRef id
-      | _ -> error
-          "cannot set an inductive type or a constructor as transparent" in
+      | _ -> user_err Pp.(str
+          "cannot set an inductive type or a constructor as transparent") in
   let l = List.map glob_ref l in
   Redexpr.set_strategy local [v,l]
 
@@ -1764,10 +1764,10 @@ let vernac_locate = let open Feedback in function
 
 let vernac_register id r =
  if Pfedit.refining () then
-    error "Cannot register a primitive while in proof editing mode.";
+    user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
   let t = (Constrintern.global_reference (snd id)) in
   if not (isConst t) then
-    error "Register inline: a constant is expected";
+    user_err Pp.(str "Register inline: a constant is expected");
   let kn = destConst t in
   match r with
   | RegisterInline -> Global.register_inline (Univ.out_punivs kn)
@@ -1780,7 +1780,7 @@ let vernac_focus gln =
     match gln with
       | None -> Proof.focus focus_command_cond () 1 p
       | Some 0 ->
-         CErrors.error "Invalid goal number: 0. Goal numbering starts with 1."
+         user_err Pp.(str "Invalid goal number: 0. Goal numbering starts with 1.")
       | Some n ->
          Proof.focus focus_command_cond () n p)
 
@@ -1795,7 +1795,7 @@ let vernac_unfocused () =
   if Proof.unfocused p then
     Feedback.msg_notice (str"The proof is indeed fully unfocused.")
   else
-    error "The proof is not fully unfocused."
+    user_err Pp.(str "The proof is not fully unfocused.")
 
 
 (* BeginSubproof / EndSubproof. 
@@ -2081,7 +2081,7 @@ let check_vernac_supports_locality c l =
     | VernacDeclareReduction _
     | VernacExtend _ 
     | VernacInductive _) -> ()
-  | Some _, _ -> CErrors.error "This command does not support Locality"
+  | Some _, _ -> user_err Pp.(str "This command does not support Locality")
 
 (* Vernaculars that take a polymorphism flag *)
 let check_vernac_supports_polymorphism c p =
@@ -2095,7 +2095,7 @@ let check_vernac_supports_polymorphism c p =
     | VernacInstance _ | VernacDeclareInstances _
     | VernacHints _ | VernacContext _
     | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> ()
-  | Some _, _ -> CErrors.error "This command does not support Polymorphism"
+  | Some _, _ -> user_err Pp.(str "This command does not support Polymorphism")
 
 let enforce_polymorphism = function
   | None -> Flags.is_universe_polymorphism ()
@@ -2172,13 +2172,13 @@ let interp ?(verbosely=true) ?proof (loc,c) =
     | VernacStm _ -> assert false (* Done by Stm *)
 
     | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
-    | VernacProgram _ -> CErrors.error "Program mode specified twice"
+    | VernacProgram _ -> user_err Pp.(str "Program mode specified twice")
     | VernacLocal (b, c) when Option.is_empty locality -> 
       aux ~locality:b ?polymorphism isprogcmd c
     | VernacPolymorphic (b, c) when polymorphism = None -> 
       aux ?locality ~polymorphism:b isprogcmd c
-    | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice"
-    | VernacLocal _ -> CErrors.error "Locality specified twice"
+    | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice")
+    | VernacLocal _ -> user_err Pp.(str "Locality specified twice")
     | VernacFail v ->
         with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v)
     | VernacTimeout (n,v) ->