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

10 files changed, 27 insertions, 27 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 11678fa6b..6d93c11ea 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -72,7 +72,7 @@ let find_library dir =
 let try_find_library dir =
   try find_library dir
   with Not_found ->
-    error ("Unknown library " ^ (DirPath.to_string dir))
+    user_err Pp.(str ("Unknown library " ^ (DirPath.to_string dir)))
 
 let library_full_filename dir = (find_library dir).library_filename
 
diff --git a/checker/checker.ml b/checker/checker.ml
index 5cadfe7b9..e00f47a54 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -335,7 +335,7 @@ let parse_args argv =
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-where" :: _ ->
-        Envars.set_coqlib ~fail:CErrors.error;
+        Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
         print_endline (Envars.coqlib ());
         exit 0
 
@@ -373,7 +373,7 @@ let init_with_argv argv =
     try
       parse_args argv;
       if !Flags.debug then Printexc.record_backtrace true;
-      Envars.set_coqlib ~fail:CErrors.error;
+      Envars.set_coqlib ~fail:(fun x -> CErrors.user_err Pp.(str x));
       if_verbose print_header ();
       init_load_path ();
       engage ();
diff --git a/checker/environ.ml b/checker/environ.ml
index 7b59c6b98..bce40861c 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -45,7 +45,7 @@ let set_engagement (impr_set as c) env =
     env.env_stratification.env_engagement in
   begin
     match impr_set,expected_impr_set with
-    | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
+    | PredicativeSet, ImpredicativeSet -> user_err Pp.(str "Incompatible engagement")
     | _ -> ()
   end;
   { env with env_stratification =
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 27f79e796..0482912b0 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -535,13 +535,13 @@ let check_inductive env kn mib =
   (* check mind_finite : always OK *)
   (* check mind_ntypes *)
   if Array.length mib.mind_packets <> mib.mind_ntypes then
-    error "not the right number of packets";
+    user_err Pp.(str "not the right number of packets");
   (* check mind_params_ctxt *)
   let params = mib.mind_params_ctxt in
   let _ = check_ctxt env params in
   (* check mind_nparams *)
   if rel_context_nhyps params <> mib.mind_nparams then
-    error "number the right number of parameters";
+    user_err Pp.(str "number the right number of parameters");
   (* mind_packets *)
   (*  - check arities *)
   let env_ar = typecheck_arity env params mib.mind_packets in
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 8f23a38af..9e417a8eb 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -27,7 +27,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body
 let lookup_mind_specif env (kn,tyi) =
   let mib = lookup_mind kn env in
   if tyi >= Array.length mib.mind_packets then
-    error "Inductive.lookup_mind_specif: invalid inductive index";
+    user_err Pp.(str "Inductive.lookup_mind_specif: invalid inductive index");
   (mib, mib.mind_packets.(tyi))
 
 let find_rectype env c =
@@ -232,7 +232,7 @@ let type_of_constructor_subst cstr u (mib,mip) =
   let specif = mip.mind_user_lc in
   let i = index_of_constructor cstr in
   let nconstr = Array.length mip.mind_consnames in
-  if i > nconstr then error "Not enough constructors in the type.";
+  if i > nconstr then user_err Pp.(str "Not enough constructors in the type.");
     constructor_instantiate (fst ind) u mib specif.(i-1)
 
 let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
diff --git a/checker/modops.ml b/checker/modops.ml
index 07dda8a06..bed31143b 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -16,21 +16,21 @@ open Declarations
 (*i*)
 
 let error_not_a_constant l =
-  error ("\""^(Label.to_string l)^"\" is not a constant")
+  user_err Pp.(str ("\""^(Label.to_string l)^"\" is not a constant"))
 
-let error_not_a_functor () = error "Application of not a functor"
+let error_not_a_functor () = user_err Pp.(str "Application of not a functor")
 
-let error_incompatible_modtypes _ _ = error "Incompatible module types"
+let error_incompatible_modtypes _ _ = user_err Pp.(str "Incompatible module types")
 
 let error_not_match l _ =
-  error ("Signature components for label "^Label.to_string l^" do not match")
+  user_err Pp.(str ("Signature components for label "^Label.to_string l^" do not match"))
 
-let error_no_such_label l = error ("No such label "^Label.to_string l)
+let error_no_such_label l = user_err Pp.(str ("No such label "^Label.to_string l))
 
 let error_no_such_label_sub l l1 =
   let l1 = ModPath.to_string l1 in
-  error ("The field "^
-         Label.to_string l^" is missing in "^l1^".")
+  user_err Pp.(str ("The field "^
+         Label.to_string l^" is missing in "^l1^"."))
 
 let error_not_a_module_loc ?loc s =
   user_err ?loc  (str ("\""^Label.to_string s^"\" is not a module"))
@@ -38,7 +38,7 @@ let error_not_a_module_loc ?loc s =
 let error_not_a_module s = error_not_a_module_loc s
 
 let error_with_module () =
-  error "Unsupported 'with' constraint in module implementation"
+  user_err Pp.(str "Unsupported 'with' constraint in module implementation")
 
 let is_functor = function
   | MoreFunctor _ -> true
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 28c0126b4..82f09cf4b 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -536,5 +536,5 @@ let dest_arity env c =
   let l, c = dest_prod_assum env c in
   match c with
     | Sort s -> l,s
-    | _ -> error "not an arity"
+    | _ -> user_err Pp.(str "not an arity")
 
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 53d80c6d5..c70cd5c8c 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -40,7 +40,7 @@ let check_engagement env expected_impredicative_set =
   begin
     match impredicative_set, expected_impredicative_set with
     | PredicativeSet, ImpredicativeSet ->
-        CErrors.error "Needs option -impredicative-set."
+        CErrors.user_err Pp.(str "Needs option -impredicative-set.")
     | _ -> ()
   end;
   ()
@@ -61,7 +61,7 @@ let check_imports f caller env needed =
       let actual_stamp = lookup_digest env dp in
       if stamp <> actual_stamp then report_clash f caller dp
     with Not_found ->
-      error ("Reference to unknown module " ^ (DirPath.to_string dp))
+      user_err Pp.(str ("Reference to unknown module " ^ (DirPath.to_string dp)))
   in
   Array.iter check needed
 
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index a290b240d..2d04b77e4 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -302,22 +302,22 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		let c2 = force_constr lc2 in
 		check_conv conv env c1 c2))
       | IndType ((kn,i),mind1) ->
-	  ignore (CErrors.error (
+	  ignore (CErrors.user_err (Pp.str (
 		    "The kernel does not recognize yet that a parameter can be " ^
 		      "instantiated by an inductive type. Hint: you can rename the " ^
 		      "inductive type and give a definition to map the old name to the new " ^
-		      "name."));
+		      "name.")));
       if constant_has_body cb2 then error () ;
       let u = inductive_instance mind1 in
       let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
-      ignore (CErrors.error (
+      ignore (CErrors.user_err (Pp.str (
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
-       "name."));
+       "name.")));
       if constant_has_body cb2 then error () ;
       let u1 = inductive_instance mind1 in
       let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
diff --git a/checker/term.ml b/checker/term.ml
index 24e6008d3..8cac78375 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -273,14 +273,14 @@ let decompose_lam =
   abstractions *)
 let decompose_lam_n_assum n =
   if n < 0 then
-    error "decompose_lam_n_assum: integer parameter must be positive";
+    user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive");
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else match c with
     | Lambda (x,t,c)  -> lamdec_rec (LocalAssum (x,t) :: l) (n-1) c
     | LetIn (x,b,t,c) -> lamdec_rec (LocalDef (x,b,t) :: l) n c
     | Cast (c,_,_)      -> lamdec_rec l n c
-    | c -> error "decompose_lam_n_assum: not enough abstractions"
+    | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions")
   in
   lamdec_rec empty_rel_context n
 
@@ -306,14 +306,14 @@ let decompose_prod_assum =
 
 let decompose_prod_n_assum n =
   if n < 0 then
-    error "decompose_prod_n_assum: integer parameter must be positive";
+    user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive");
   let rec prodec_rec l n c =
     if Int.equal n 0 then l,c
     else match c with
     | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) (n-1) c
     | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) (n-1) c
     | Cast (c,_,_)    -> prodec_rec l n c
-    | c -> error "decompose_prod_n_assum: not enough assumptions"
+    | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions")
   in
   prodec_rec empty_rel_context n