Merge PR#512: [cleanup] Unify all calls to the error function.

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