Reuse the typing_flags datatype for inductives.

6 files changed, 9 insertions, 14 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index ef4d398c1..f89773fcc 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -190,11 +190,8 @@ type mutual_inductive_body = {
     mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
-  
-    mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker.  *)
-
-    mind_unsafe_universes : bool; (** generated with the type-in-type flag *)
 
+    mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)
 }
 
 (** {6 Module declarations } *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 5caf052ac..211e5e062 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -261,8 +261,7 @@ let subst_mind_body sub mib =
     mind_polymorphic = mib.mind_polymorphic;
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private;
-    mind_checked_positive = mib.mind_checked_positive;
-    mind_unsafe_universes = mib.mind_unsafe_universes;
+    mind_typing_flags = mib.mind_typing_flags;
   }
 
 let inductive_instance mib =
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 8b29e3abd..df2c4653f 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -52,8 +52,6 @@ type mutual_inductive_entry = {
   mind_entry_polymorphic : bool; 
   mind_entry_universes : Univ.universe_context;
   mind_entry_private : bool option;
-  mind_entry_check_positivity : bool;
-  (** [false] if positivity is to be assumed. *)
 }
 
 (** {6 Constants (Definition/Axiom) } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 65aaa3f7b..9fb3bf79f 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -53,6 +53,7 @@ let is_impredicative_set env =
   | _ -> false
 
 let type_in_type env = not (typing_flags env).check_universes
+let deactivated_guard env = not (typing_flags env).check_guarded
 
 let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context
@@ -362,7 +363,7 @@ let polymorphic_pind (ind,u) env =
   else polymorphic_ind ind env
 
 let type_in_type_ind (mind,i) env =
-  (lookup_mind mind env).mind_unsafe_universes
+  not (lookup_mind mind env).mind_typing_flags.check_universes
 
 let template_polymorphic_ind (mind,i) env =
   match (lookup_mind mind env).mind_packets.(i).mind_arity with 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 0edcb34de..b5e576435 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -53,6 +53,7 @@ val engagement    : env -> engagement
 val typing_flags    : env -> typing_flags
 val is_impredicative_set : env -> bool
 val type_in_type : env -> bool
+val deactivated_guard : env -> bool
 
 (** is the local context empty *)
 val empty_context : env -> bool
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