diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/cic.mli | 2 | ||||
| -rw-r--r-- | checker/indtypes.ml | 7 | ||||
| -rw-r--r-- | checker/inductive.ml | 2 | ||||
| -rw-r--r-- | checker/reduction.ml | 5 | ||||
| -rw-r--r-- | checker/values.ml | 4 |
5 files changed, 10 insertions, 10 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 4162903b04..754cc2a096 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -221,6 +221,8 @@ type typing_flags = { check_universes : bool; (** If [false] universe constraints are not checked *) conv_oracle : oracle; (** Unfolding strategies for conversion *) share_reduction : bool; (** Use by-need reduction algorithm *) + enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *) + enable_native_compiler : bool; (** If [false], all native conversions fall back to VM ones *) } type constant_body = { diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 50e65ef587..f6c510ee1c 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -531,10 +531,11 @@ let check_positivity env_ar mind params nrecp inds = Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in let lra_ind = List.rev (Array.to_list rc) in let lparams = rel_context_length params in + let ra_env = + List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in + let env_ar_par = push_rel_context params env_ar in let check_one i mip = - let ra_env = - List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in - let ienv = (env_ar, 1+lparams, ntypes, ra_env) in + let ienv = (env_ar_par, 1+lparams, ntypes, ra_env) in check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc in let irecargs = Array.mapi check_one inds in diff --git a/checker/inductive.ml b/checker/inductive.ml index 5e34f04f51..269a98cb0e 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -388,7 +388,7 @@ let type_case_branches env (pind,largs) (p,pj) c = let check_case_info env indsp ci = let mib, mip as spec = lookup_mind_specif env indsp in if - not (eq_ind_chk indsp ci.ci_ind) || + not (mind_equiv env indsp ci.ci_ind) || (mib.mind_nparams <> ci.ci_npar) || (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) || (mip.mind_consnrealargs <> ci.ci_cstr_nargs) || diff --git a/checker/reduction.ml b/checker/reduction.ml index 58a3f4e410..1158152f63 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -192,10 +192,7 @@ let convert_constructors | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2 | Cumulative_ind cumi -> let num_cnstr_args = - let nparamsctxt = - mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs - in - nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1) + mind.mind_nparams + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1) in if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then convert_universes univs u1 u2 diff --git a/checker/values.ml b/checker/values.ml index 24f10b7a87..8f6b24ec26 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 a127e0c2322c7846914bbca9921309c7 checker/cic.mli +MD5 b8f0139f14e3370cd0a45d4cf69882ea checker/cic.mli *) @@ -230,7 +230,7 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] let v_typing_flags = - v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool|] + v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|] let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|] |