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

8 files changed, 28 insertions, 30 deletions

diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 3f1cf92487..4533169804 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -71,7 +71,7 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l =
     | _ -> Cpred.add c oracle.cst_trstate
     in
     { oracle with cst_opacity; cst_trstate; }
-  | RelKey _ -> CErrors.error "set_strategy: RelKey"
+  | RelKey _ -> CErrors.user_err Pp.(str "set_strategy: RelKey")
 
 let fold_strategy f { var_opacity; cst_opacity; } accu =
   let fvar id lvl accu = f (VarKey id) lvl accu in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d8d365c347..4f4b641b44 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -25,7 +25,7 @@ type mind_specif = mutual_inductive_body * one_inductive_body
 let lookup_mind_specif env (kn,tyi) =
   let mib = Environ.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 =
@@ -247,7 +247,7 @@ let type_of_constructor (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 constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) =
diff --git a/kernel/names.ml b/kernel/names.ml
index f5b3f4e007..afdbe0c0dc 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -35,7 +35,7 @@ struct
   let hash = String.hash
 
   let check_valid ?(strict=true) x =
-    let iter (fatal, x) = if fatal || strict then CErrors.error x in
+    let iter (fatal, x) = if fatal || strict then CErrors.user_err Pp.(str x) in
     Option.iter iter (Unicode.ident_refutation x)
 
   let is_valid s = match Unicode.ident_refutation s with
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 6bd82170e6..26d0617683 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -125,7 +125,7 @@ let call_linker ?(fatal=true) prefix f upds =
   if not (Sys.file_exists f) then
     begin
       let msg = "Cannot find native compiler file " ^ f in
-      if fatal then CErrors.error msg
+      if fatal then CErrors.user_err Pp.(str msg)
       else if !Flags.debug then Feedback.msg_debug (Pp.str msg)
     end
   else
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index d0593c0e05..502a10113d 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -36,12 +36,11 @@ let empty_opaquetab = {
 
 (* hooks *)
 let default_get_opaque dp _ =
-  CErrors.error
-    ("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
+  CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp])
 let default_get_univ dp _ =
-  CErrors.error
-    ("Cannot access universe constraints of opaque proofs in library " ^
-    DirPath.to_string dp)
+  CErrors.user_err (Pp.pr_sequence Pp.str [
+    "Cannot access universe constraints of opaque proofs in library ";
+    DirPath.to_string dp])
 
 let get_opaque = ref default_get_opaque
 let get_univ = ref default_get_univ
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index caaaff1b89..f5e8e86530 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -192,7 +192,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
 
@@ -346,10 +346,10 @@ let check_required current_libs needed =
     try
       let actual = DPMap.find id current_libs in
       if not(digest_match ~actual ~required) then
-        CErrors.error
-          ("Inconsistent assumptions over module "^(DirPath.to_string id)^".")
+        CErrors.user_err Pp.(pr_sequence str
+          ["Inconsistent assumptions over module"; DirPath.to_string id; "."])
     with Not_found ->
-      CErrors.error ("Reference to unknown module "^(DirPath.to_string id)^".")
+      CErrors.user_err Pp.(pr_sequence str ["Reference to unknown module"; DirPath.to_string id; "."])
   in
   Array.iter check needed
 
@@ -367,7 +367,7 @@ let safe_push_named d env =
   let _ =
     try
       let _ = Environ.lookup_named id env in
-      CErrors.error ("Identifier "^Id.to_string id^" already defined.")
+      CErrors.user_err Pp.(pr_sequence str ["Identifier"; Id.to_string id; "already defined."])
     with Not_found -> () in
   Environ.push_named d env
 
@@ -908,7 +908,7 @@ let register_inline kn senv =
   let open Environ in
   let open Pre_env in
   if not (evaluable_constant kn senv.env) then
-    CErrors.error "Register inline: an evaluable constant is expected";
+    CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected");
   let env = pre_env senv.env in
   let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in
   let cb = {cb with const_inline_code = true} in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index d0fdf9fdae..f779f68be4 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -110,8 +110,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   in
   let u = 
     if poly then 
-      CErrors.error ("Checking of subtyping of polymorphic" ^
-		       " inductive types not implemented")
+      CErrors.user_err Pp.(str "Checking of subtyping of polymorphic inductive types not implemented")
     else Instance.empty
   in
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
@@ -347,7 +346,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 	      let c2 = Mod_subst.force_constr lc2 in
 	      check_conv NotConvertibleBodyField cst poly u infer_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 " ^
@@ -364,7 +363,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
       let error = NotConvertibleTypeField (env, arity1, typ2) in
        check_conv error cst false Univ.Instance.empty infer_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 " ^
diff --git a/kernel/term.ml b/kernel/term.ml
index 03562d9f31..a4296a530c 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -526,26 +526,26 @@ let decompose_lam =
 (* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T
    into the pair ([(xn,Tn);...;(x1,T1)],T) *)
 let decompose_prod_n n =
-  if n < 0 then error "decompose_prod_n: integer parameter must be positive";
+  if n < 0 then user_err (str "decompose_prod_n: integer parameter must be positive");
   let rec prodec_rec l n c =
     if Int.equal n 0 then l,c
     else match kind_of_term c with
       | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c
       | Cast (c,_,_)   -> prodec_rec l n c
-      | _ -> error "decompose_prod_n: not enough products"
+      | _ -> user_err (str "decompose_prod_n: not enough products")
   in
   prodec_rec [] n
 
 (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
    into the pair ([(xn,Tn);...;(x1,T1)],T) *)
 let decompose_lam_n n =
-  if n < 0 then error "decompose_lam_n: integer parameter must be positive";
+  if n < 0 then user_err (str "decompose_lam_n: integer parameter must be positive");
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else match kind_of_term c with
       | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
       | Cast (c,_,_)     -> lamdec_rec l n c
-      | _ -> error "decompose_lam_n: not enough abstractions"
+      | _ -> user_err (str "decompose_lam_n: not enough abstractions")
   in
   lamdec_rec [] n
 
@@ -581,7 +581,7 @@ let decompose_lam_assum =
    ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *)
 let decompose_prod_n_assum n =
   if n < 0 then
-    error "decompose_prod_n_assum: integer parameter must be positive";
+    user_err (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
@@ -590,7 +590,7 @@ let decompose_prod_n_assum n =
       | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (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 (str  "decompose_prod_n_assum: not enough assumptions")
   in
   prodec_rec Context.Rel.empty n
 
@@ -602,7 +602,7 @@ let decompose_prod_n_assum n =
    but n is the actual number of destructurated lambdas. *)
 let decompose_lam_n_assum n =
   if n < 0 then
-    error "decompose_lam_n_assum: integer parameter must be positive";
+    user_err (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
@@ -611,14 +611,14 @@ let decompose_lam_n_assum n =
       | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (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 (str "decompose_lam_n_assum: not enough abstractions")
   in
   lamdec_rec Context.Rel.empty n
 
 (* Same, counting let-in *)
 let decompose_lam_n_decls n =
   if n < 0 then
-    error "decompose_lam_n_decls: integer parameter must be positive";
+    user_err (str "decompose_lam_n_decls: integer parameter must be positive");
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else
@@ -627,7 +627,7 @@ let decompose_lam_n_decls n =
       | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> lamdec_rec l n c
-      | c -> error "decompose_lam_n_decls: not enough abstractions"
+      | c -> user_err (str "decompose_lam_n_decls: not enough abstractions")
   in
   lamdec_rec Context.Rel.empty n