Reuse the typing_flags datatype for inductives.

1 files changed, 4 insertions, 5 deletions

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