aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/conv_oracle.ml2
-rw-r--r--kernel/inductive.ml4
-rw-r--r--kernel/names.ml2
-rw-r--r--kernel/nativelib.ml2
-rw-r--r--kernel/opaqueproof.ml9
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--kernel/subtyping.ml7
-rw-r--r--kernel/term.ml20
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:24:49 +0000