aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml13
-rw-r--r--checker/check.mllib3
-rw-r--r--checker/check_stat.ml3
-rw-r--r--checker/checker.ml18
-rw-r--r--checker/environ.ml2
-rw-r--r--checker/include2
-rw-r--r--checker/indtypes.ml16
-rw-r--r--checker/inductive.ml88
-rw-r--r--checker/modops.ml2
-rw-r--r--checker/print.ml6
-rw-r--r--checker/reduction.ml16
-rw-r--r--checker/reduction.mli4
-rw-r--r--checker/safe_typing.ml4
-rw-r--r--checker/subtyping.ml6
-rw-r--r--checker/term.ml2
-rw-r--r--checker/typeops.ml6
-rw-r--r--checker/univ.ml2
17 files changed, 79 insertions, 114 deletions
diff --git a/checker/check.ml b/checker/check.ml
index da3cd03161..8b299bf2a2 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -7,10 +7,12 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
+let chk_pp = Pp.pp_with Format.std_formatter
+
let pr_dirpath dp = str (DirPath.to_string dp)
let default_root_prefix = DirPath.empty
let split_dirpath d =
@@ -118,7 +120,6 @@ let check_one_lib admit (dir,m) =
(Flags.if_verbose Feedback.msg_notice
(str "Checking library: " ++ pr_dirpath dir);
Safe_typing.import file md m.library_extra_univs dig);
- Flags.if_verbose Feedback.msg_notice (fnl());
register_loaded_library m
(*************************************************************************)
@@ -298,7 +299,7 @@ let name_clash_message dir mdir f =
let depgraph = ref LibraryMap.empty
let intern_from_file (dir, f) =
- Flags.if_verbose Feedback.msg_notice(str"[intern "++str f++str" ...");
+ Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
let (sd,md,table,opaque_csts,digest) =
try
let ch = System.with_magic_number_check raw_intern_library f in
@@ -322,7 +323,7 @@ let intern_from_file (dir, f) =
errorlabstrm "intern_from_file"
(str "The file "++str f++str " contains unfinished tasks");
if opaque_csts <> None then begin
- Feedback.msg_notice(str " (was a vio file) ");
+ chk_pp (str " (was a vio file) ");
Option.iter (fun (_,_,b) -> if not b then
errorlabstrm "intern_from_file"
(str "The file "++str f++str " is still a .vio"))
@@ -333,12 +334,12 @@ let intern_from_file (dir, f) =
Validate.validate !Flags.debug Values.v_libsum sd;
Validate.validate !Flags.debug Values.v_lib md;
Validate.validate !Flags.debug Values.v_opaques table;
- Flags.if_verbose Feedback.msg_notice (str" done]");
+ Flags.if_verbose chk_pp (str" done]" ++ fnl ());
let digest =
if opaque_csts <> None then Cic.Dviovo (digest,udg)
else (Cic.Dvo digest) in
sd,md,table,opaque_csts,digest
- with e -> Flags.if_verbose Feedback.msg_notice (str" failed!]"); raise e in
+ with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in
depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph;
opaque_tables := LibraryMap.add sd.md_name table !opaque_tables;
Option.iter (fun (opaque_csts,_,_) ->
diff --git a/checker/check.mllib b/checker/check.mllib
index 2fa4d57977..488507a13f 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -34,7 +34,8 @@ Feedback
Segmenttree
Unicodetable
Unicode
-Errors
+CErrors
+CWarnings
CEphemeron
Future
CUnix
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index f196746a57..741f532848 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -57,8 +57,7 @@ let print_context env =
(fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
str"===============" ++ fnl() ++ fnl() ++
str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
- str "* " ++ hov 0 (pr_ax csts) ++
- fnl()));
+ str "* " ++ hov 0 (pr_ax csts)));
end
let stats () =
diff --git a/checker/checker.ml b/checker/checker.ml
index 2c872f2721..8dbb7e0119 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open System
open Flags
@@ -16,6 +16,8 @@ open Check
let () = at_exit flush_all
+let chk_pp = Pp.pp_with Format.std_formatter
+
let fatal_error info anomaly =
flush_all (); Feedback.msg_error info; flush_all ();
exit (if anomaly then 129 else 1)
@@ -71,7 +73,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
let convert_string d =
try Id.of_string d
- with Errors.UserError _ ->
+ with CErrors.UserError _ ->
if_verbose Feedback.msg_warning
(str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)");
raise Exit
@@ -209,7 +211,8 @@ let usage () =
open Type_errors
let anomaly_string () = str "Anomaly: "
-let report () = (str "." ++ spc () ++ str "Please report.")
+let report () = (str "." ++ spc () ++ str "Please report" ++
+ strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".")
let guill s = str "\"" ++ str s ++ str "\""
@@ -282,7 +285,8 @@ let rec explain_exn = function
Format.printf "@\nis not convertible with@\n";
Print.print_pure_constr a;
Format.printf "@\n====== universes ====@\n";
- Feedback.msg_notice (Univ.pr_universes
+ chk_pp
+ (Univ.pr_universes
(ctx.Environ.env_stratification.Environ.env_universes));
str "\nCantApplyBadType at argument " ++ int n
| CantApplyNonFunctional _ -> str"CantApplyNonFunctional"
@@ -303,7 +307,7 @@ let rec explain_exn = function
str ", characters " ++ int e ++ str "-" ++
int (e+6) ++ str ")")) ++
report ())
- | e -> Errors.print e (* for anomalies and other uncaught exceptions *)
+ | e -> CErrors.print e (* for anomalies and other uncaught exceptions *)
let parse_args argv =
let rec parse = function
@@ -329,7 +333,7 @@ let parse_args argv =
| "-debug" :: rem -> set_debug (); parse rem
| "-where" :: _ ->
- Envars.set_coqlib ~fail:Errors.error;
+ Envars.set_coqlib ~fail:CErrors.error;
print_endline (Envars.coqlib ());
exit 0
@@ -367,7 +371,7 @@ let init_with_argv argv =
try
parse_args argv;
if !Flags.debug then Printexc.record_backtrace true;
- Envars.set_coqlib ~fail:Errors.error;
+ Envars.set_coqlib ~fail:CErrors.error;
if_verbose print_header ();
init_load_path ();
engage ();
diff --git a/checker/environ.ml b/checker/environ.ml
index 881284eda7..7b59c6b986 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -1,4 +1,4 @@
-open Errors
+open CErrors
open Util
open Names
open Cic
diff --git a/checker/include b/checker/include
index f5bd2984ee..6bea3c91a7 100644
--- a/checker/include
+++ b/checker/include
@@ -31,7 +31,7 @@ open Typeops;;
open Check;;
open Pp;;
-open Errors;;
+open CErrors;;
open Util;;
open Names;;
open Term;;
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 29b16392b5..27f79e7963 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Cic
@@ -44,7 +44,7 @@ let prcon c =
let weaker_noccur_between env x nvars t =
if noccur_between x nvars t then Some t
else
- let t' = whd_betadeltaiota env t in
+ let t' = whd_all env t in
if noccur_between x nvars t' then Some t'
else None
@@ -90,7 +90,7 @@ exception InductiveError of inductive_error
(* Typing the arities and constructor types *)
let rec sorts_of_constr_args env t =
- let t = whd_betadeltaiota_nolet env t in
+ let t = whd_allnolet env t in
match t with
| Prod (name,c1,c2) ->
let varj = infer_type env c1 in
@@ -321,7 +321,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
| [] -> ()
| LocalDef _ :: hyps -> check k (index+1) hyps
| _::hyps ->
- match whd_betadeltaiota env lpar.(k) with
+ match whd_all env lpar.(k) with
| Rel w when w = index -> check (k-1) (index+1) hyps
| _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l)))
in check (nparams-1) (n-nhyps) hyps;
@@ -342,7 +342,7 @@ let check_rec_par (env,n,_,_) hyps nrecp largs =
failwith "number of recursive parameters cannot be greater than the number of parameters."
| (lp,LocalDef _ :: hyps) -> find (index-1) (lp,hyps)
| (p::lp,_::hyps) ->
- (match whd_betadeltaiota env p with
+ (match whd_all env p with
| Rel w when w = index -> find (index-1) (lp,hyps)
| _ -> failwith "bad number of recursive parameters")
in find (n-1) (lpar,List.rev hyps)
@@ -388,7 +388,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lpar) =
let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
if n=0 then (ienv,c) else
- let c' = whd_betadeltaiota env c in
+ let c' = whd_all env c in
match c' with
Prod(na,a,b) ->
let ienv' = ienv_push_var ienv (na,a,mk_norec) in
@@ -401,7 +401,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
let lparams = rel_context_length hyps in
(* check the inductive types occur positively in [c] *)
let rec check_pos (env, n, ntypes, ra_env as ienv) c =
- let x,largs = decompose_app (whd_betadeltaiota env c) in
+ let x,largs = decompose_app (whd_all env c) in
match x with
| Prod (na,b,d) ->
assert (List.is_empty largs);
@@ -470,7 +470,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
and check_constructors ienv check_head c =
let rec check_constr_rec (env,n,ntypes,ra_env as ienv) lrec c =
- let x,largs = decompose_app (whd_betadeltaiota env c) in
+ let x,largs = decompose_app (whd_all env c) in
match x with
| Prod (na,b,d) ->
assert (List.is_empty largs);
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 43a32ea24d..c4ffc141ff 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Cic
@@ -31,20 +31,20 @@ let lookup_mind_specif env (kn,tyi) =
(mib, mib.mind_packets.(tyi))
let find_rectype env c =
- let (t, l) = decompose_app (whd_betadeltaiota env c) in
+ let (t, l) = decompose_app (whd_all env c) in
match t with
| Ind ind -> (ind, l)
| _ -> raise Not_found
let find_inductive env c =
- let (t, l) = decompose_app (whd_betadeltaiota env c) in
+ let (t, l) = decompose_app (whd_all env c) in
match t with
| Ind (ind,_)
when (fst (lookup_mind_specif env ind)).mind_finite != CoFinite -> (ind, l)
| _ -> raise Not_found
let find_coinductive env c =
- let (t, l) = decompose_app (whd_betadeltaiota env c) in
+ let (t, l) = decompose_app (whd_all env c) in
match t with
| Ind (ind,_)
when (fst (lookup_mind_specif env ind)).mind_finite == CoFinite -> (ind, l)
@@ -59,16 +59,6 @@ let inductive_instance mib =
UContext.instance mib.mind_universes
else Instance.empty
-let inductive_context mib =
- if mib.mind_polymorphic then
- instantiate_univ_context mib.mind_universes
- else UContext.empty
-
-let instantiate_inductive_constraints mib u =
- if mib.mind_polymorphic then
- subst_instance_constraints u (UContext.constraints mib.mind_universes)
- else Constraint.empty
-
(************************************************************************)
(* Build the substitution that replaces Rels by the appropriate *)
@@ -190,8 +180,6 @@ let rec make_subst env =
in
make Univ.LMap.empty
-exception SingletonInductiveBecomesProp of Id.t
-
let instantiate_universes env ctx ar argsorts =
let args = Array.to_list argsorts in
let subst = make_subst env (ctx,ar.template_param_levels,args) in
@@ -208,11 +196,7 @@ let instantiate_universes env ctx ar argsorts =
(* Type of an inductive type *)
-let is_prop_sort = function
- | Prop Null -> true
- | _ -> false
-
-let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+let type_of_inductive_gen env ((mib,mip),u) paramtyps =
match mip.mind_arity with
| RegularArity a ->
if not mib.mind_polymorphic then a.mind_user_arity
@@ -220,25 +204,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
| TemplateArity ar ->
let ctx = List.rev mip.mind_arity_ctxt in
let ctx,s = instantiate_universes env ctx ar paramtyps in
- (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
- the situation where a non-Prop singleton inductive becomes Prop
- when applied to Prop params *)
- if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s
- then raise (SingletonInductiveBecomesProp mip.mind_typename);
- mkArity (List.rev ctx,s)
-
-let type_of_inductive env pind =
- type_of_inductive_gen env pind [||]
-
-let constrained_type_of_inductive env ((mib,mip),u as pind) =
- let ty = type_of_inductive_gen env pind [||] in
- let cst = instantiate_inductive_constraints mib u in
- (ty, cst)
-
-let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
- let ty = type_of_inductive_gen env pind args in
- let cst = instantiate_inductive_constraints mib u in
- (ty, cst)
+ mkArity (List.rev ctx,s)
let type_of_inductive_knowing_parameters env mip args =
type_of_inductive_gen env mip args
@@ -275,16 +241,6 @@ let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
let type_of_constructor cstru mspec =
type_of_constructor_gen cstru mspec
-let type_of_constructor_in_ctx cstr (mib,mip as mspec) =
- let u = Univ.UContext.instance mib.mind_universes in
- let c = type_of_constructor_gen (cstr, u) mspec in
- (c, mib.mind_universes)
-
-let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) =
- let ty = type_of_constructor_gen cstru ind in
- let cst = instantiate_inductive_constraints mib u in
- (ty, cst)
-
let arities_of_specif (kn,u) (mib,mip) =
let specif = mip.mind_nf_lc in
Array.map (constructor_instantiate kn u mib) specif
@@ -343,7 +299,7 @@ let check_allowed_sort ksort specif =
let is_correct_arity env c (p,pj) ind specif params =
let arsign,_ = get_instantiated_arity ind specif params in
let rec srec env pt ar =
- let pt' = whd_betadeltaiota env pt in
+ let pt' = whd_all env pt in
match pt', ar with
| Prod (na1,a1,t), LocalAssum (_,a1')::ar' ->
(try conv env a1 a1'
@@ -351,7 +307,7 @@ let is_correct_arity env c (p,pj) ind specif params =
srec (push_rel (LocalAssum (na1,a1)) env) t ar'
| Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
let env' = push_rel (LocalAssum (na1,a1)) env in
- let ksort = match (whd_betadeltaiota env' a2) with
+ let ksort = match (whd_all env' a2) with
| Sort s -> family_of_sort s
| _ -> raise (LocalArity None) in
let dep_ind = build_dependent_inductive ind specif params in
@@ -622,7 +578,7 @@ let check_inductive_codomain env p =
let env = push_rel_context absctx env in
let arctx, s = dest_prod_assum env ar in
let env = push_rel_context arctx env in
- let i,l' = decompose_app (whd_betadeltaiota env s) in
+ let i,l' = decompose_app (whd_all env s) in
match i with Ind _ -> true | _ -> false
(* The following functions are almost duplicated from indtypes.ml, except
@@ -646,7 +602,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) =
let rec ienv_decompose_prod (env,_ as ienv) n c =
if Int.equal n 0 then (ienv,c) else
- let c' = whd_betadeltaiota env c in
+ let c' = whd_all env c in
match c' with
Prod(na,a,b) ->
let ienv' = ienv_push_var ienv (na,a,mk_norec) in
@@ -676,7 +632,7 @@ close to check_positive in indtypes.ml, but does no positivy check and does not
compute the number of recursive arguments. *)
let get_recargs_approx env tree ind args =
let rec build_recargs (env, ra_env as ienv) tree c =
- let x,largs = decompose_app (whd_betadeltaiota env c) in
+ let x,largs = decompose_app (whd_all env c) in
match x with
| Prod (na,b,d) ->
assert (List.is_empty largs);
@@ -735,7 +691,7 @@ let get_recargs_approx env tree ind args =
and build_recargs_constructors ienv trees c =
let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c =
- let x,largs = decompose_app (whd_betadeltaiota env c) in
+ let x,largs = decompose_app (whd_all env c) in
match x with
| Prod (na,b,d) ->
@@ -764,7 +720,7 @@ let restrict_spec env spec p =
let env = push_rel_context absctx env in
let arctx, s = dest_prod_assum env ar in
let env = push_rel_context arctx env in
- let i,args = decompose_app (whd_betadeltaiota env s) in
+ let i,args = decompose_app (whd_all env s) in
match i with
| Ind i ->
begin match spec with
@@ -786,7 +742,7 @@ let restrict_spec env spec p =
let rec subterm_specif renv stack t =
(* maybe reduction is not always necessary! *)
- let f,l = decompose_app (whd_betadeltaiota renv.env t) in
+ let f,l = decompose_app (whd_all renv.env t) in
match f with
| Rel k -> subterm_var k renv
@@ -900,11 +856,11 @@ let filter_stack_domain env ci p stack =
if noccur_with_meta 1 (rel_context_length absctx) ar then stack
else let env = push_rel_context absctx env in
let rec filter_stack env ar stack =
- let t = whd_betadeltaiota env ar in
+ let t = whd_all env ar in
match stack, t with
| elt :: stack', Prod (n,a,c0) ->
let d = LocalAssum (n,a) in
- let ty, args = decompose_app (whd_betadeltaiota env a) in
+ let ty, args = decompose_app (whd_all env a) in
let elt = match ty with
| Ind ind ->
let spec' = stack_element_specif elt in
@@ -1033,6 +989,10 @@ let check_one_fix renv recpos trees def =
| (Ind _ | Construct _) ->
List.iter (check_rec_call renv []) l
+ | Proj (p, c) ->
+ List.iter (check_rec_call renv []) l;
+ check_rec_call renv [] c
+
| Var _ -> anomaly (Pp.str "Section variable in Coqchk !")
| Sort _ -> assert (l = [])
@@ -1042,8 +1002,6 @@ let check_one_fix renv recpos trees def =
| (App _ | LetIn _ | Cast _) -> assert false (* beta zeta reduction *)
- | Proj (p, c) -> check_rec_call renv [] c
-
and check_nested_fix_body renv decr recArgsDecrArg body =
if decr = 0 then
check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body
@@ -1076,7 +1034,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
(* check fi does not appear in the k+1 first abstractions,
gives the type of the k+1-eme abstraction (must be an inductive) *)
let rec check_occur env n def =
- match (whd_betadeltaiota env def) with
+ match (whd_all env def) with
| Lambda (x,a,b) ->
if noccur_with_meta n nbfix a then
let env' = push_rel (LocalAssum (x,a)) env in
@@ -1125,7 +1083,7 @@ let anomaly_ill_typed () =
anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor")
let rec codomain_is_coind env c =
- let b = whd_betadeltaiota env c in
+ let b = whd_all env c in
match b with
| Prod (x,a,b) ->
codomain_is_coind (push_rel (LocalAssum (x,a)) env) b
@@ -1137,7 +1095,7 @@ let rec codomain_is_coind env c =
let check_one_cofix env nbfix def deftype =
let rec check_rec_call env alreadygrd n tree vlra t =
if not (noccur_with_meta n nbfix t) then
- let c,args = decompose_app (whd_betadeltaiota env t) in
+ let c,args = decompose_app (whd_all env t) in
match c with
| Rel p when n <= p && p < n+nbfix ->
(* recursive call: must be guarded and no nested recursive
diff --git a/checker/modops.ml b/checker/modops.ml
index 442f999bb3..b720fb6213 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -7,7 +7,7 @@
(************************************************************************)
(*i*)
-open Errors
+open CErrors
open Util
open Pp
open Names
diff --git a/checker/print.ml b/checker/print.ml
index c0d1ac3688..7ef752b002 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -10,7 +10,9 @@ open Format
open Cic
open Names
-let print_instance i = Feedback.msg_notice (Univ.Instance.pr i)
+let chk_pp = Pp.pp_with Format.std_formatter
+
+let print_instance i = chk_pp (Univ.Instance.pr i)
let print_pure_constr csr =
let rec term_display c = match c with
@@ -108,7 +110,7 @@ let print_pure_constr csr =
and sort_display = function
| Prop(Pos) -> print_string "Set"
| Prop(Null) -> print_string "Prop"
- | Type u -> print_string "Type("; Feedback.msg_notice (Univ.pr_uni u); print_string ")"
+ | Type u -> print_string "Type("; chk_pp (Univ.pr_uni u); print_string ")"
and name_display = function
| Name id -> print_string (Id.to_string id)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index b280df54a2..ec16aa2615 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Cic
open Term
@@ -92,13 +92,13 @@ let whd_betaiotazeta x =
Prod _|Lambda _|Fix _|CoFix _) -> x
| _ -> whd_val (create_clos_infos betaiotazeta empty_env) (inject x)
-let whd_betadeltaiota env t =
+let whd_all env t =
match t with
| (Sort _|Meta _|Evar _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _) -> t
| _ -> whd_val (create_clos_infos betadeltaiota env) (inject t)
-let whd_betadeltaiota_nolet env t =
+let whd_allnolet env t =
match t with
| (Sort _|Meta _|Evar _|Ind _|Construct _|
Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t
@@ -477,7 +477,7 @@ let vm_conv cv_pb = fconv cv_pb true
* error message. *)
let hnf_prod_app env t n =
- match whd_betadeltaiota env t with
+ match whd_all env t with
| Prod (_,_,b) -> subst1 n b
| _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product")
@@ -488,7 +488,7 @@ let hnf_prod_applist env t nl =
let dest_prod env =
let rec decrec env m c =
- let t = whd_betadeltaiota env c in
+ let t = whd_all env c in
match t with
| Prod (n,a,c0) ->
let d = LocalAssum (n,a) in
@@ -500,7 +500,7 @@ let dest_prod env =
(* The same but preserving lets in the context, not internal ones. *)
let dest_prod_assum env =
let rec prodec_rec env l ty =
- let rty = whd_betadeltaiota_nolet env ty in
+ let rty = whd_allnolet env ty in
match rty with
| Prod (x,t,c) ->
let d = LocalAssum (x,t) in
@@ -510,7 +510,7 @@ let dest_prod_assum env =
prodec_rec (push_rel d env) (d::l) c
| Cast (c,_,_) -> prodec_rec env l c
| _ ->
- let rty' = whd_betadeltaiota env rty in
+ let rty' = whd_all env rty in
if Term.eq_constr rty' rty then l, rty
else prodec_rec env l rty'
in
@@ -518,7 +518,7 @@ let dest_prod_assum env =
let dest_lam_assum env =
let rec lamec_rec env l ty =
- let rty = whd_betadeltaiota_nolet env ty in
+ let rty = whd_allnolet env ty in
match rty with
| Lambda (x,t,c) ->
let d = LocalAssum (x,t) in
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 2f551f4a6c..15a2df1f14 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -16,8 +16,8 @@ open Environ
(*s Reduction functions *)
val whd_betaiotazeta : constr -> constr
-val whd_betadeltaiota : env -> constr -> constr
-val whd_betadeltaiota_nolet : env -> constr -> constr
+val whd_all : env -> constr -> constr
+val whd_allnolet : env -> constr -> constr
(************************************************************************)
(*s conversion functions *)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index e644febe45..11cd742ba4 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Cic
open Names
@@ -40,7 +40,7 @@ let check_engagement env expected_impredicative_set =
begin
match impredicative_set, expected_impredicative_set with
| PredicativeSet, ImpredicativeSet ->
- Errors.error "Needs option -impredicative-set."
+ CErrors.error "Needs option -impredicative-set."
| _ -> ()
end;
()
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 46d21f6ccb..7eae9b8310 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -7,7 +7,7 @@
(************************************************************************)
(*i*)
-open Errors
+open CErrors
open Util
open Names
open Cic
@@ -302,7 +302,7 @@ 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 (Errors.error (
+ ignore (CErrors.error (
"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 " ^
@@ -313,7 +313,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
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 (Errors.error (
+ ignore (CErrors.error (
"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/checker/term.ml b/checker/term.ml
index 56cc9cdc22..591348cb69 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -8,7 +8,7 @@
(* This module instantiates the structure of generic deBruijn terms to Coq *)
-open Errors
+open CErrors
open Util
open Names
open Esubst
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 0c7e538be2..173e19ce1b 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Names
open Cic
@@ -33,7 +33,7 @@ let check_constraints cst env =
(* This should be a type (a priori without intension to be an assumption) *)
let type_judgment env (c,ty as j) =
- match whd_betadeltaiota env ty with
+ match whd_all env ty with
| Sort s -> (c,s)
| _ -> error_not_type env j
@@ -107,7 +107,7 @@ let judge_of_apply env (f,funj) argjv =
let rec apply_rec n typ = function
| [] -> typ
| (h,hj)::restjl ->
- (match whd_betadeltaiota env typ with
+ (match whd_all env typ with
| Prod (_,c1,c2) ->
(try conv_leq env hj c1
with NotConvertible ->
diff --git a/checker/univ.ml b/checker/univ.ml
index 96d8270137..668f3a0584 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -14,7 +14,7 @@
(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *)
open Pp
-open Errors
+open CErrors
open Util
(* Universes are stratified by a partial ordering $\le$.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 04:11:14 +0000