From ecb032467557631ea60324c6afa55c91c133e40d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 17 Jun 2016 20:26:35 +0200 Subject: Reuse the typing_flags datatype for inductives. --- kernel/indtypes.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) (limited to 'kernel/indtypes.ml') diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 34771034c..b6942e133 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -816,7 +816,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs is_checked = +let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in @@ -922,8 +922,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_polymorphic = p; mind_universes = ctx; mind_private = prv; - mind_checked_positive = is_checked; - mind_unsafe_universes = type_in_type env; + mind_typing_flags = Environ.typing_flags env; } (************************************************************************) @@ -932,11 +931,11 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let check_inductive env kn mie = (* First type-check the inductive definition *) let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in - let chkpos = mie.mind_entry_check_positivity in (* Then check positivity conditions *) + let chkpos = (Environ.typing_flags env).check_guarded in let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite - inds nmr recargs chkpos + inds nmr recargs -- cgit v1.2.3