Add a corresponding field in `mutual_inductive_entry` (part 1).

The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been.

6 files changed, 15 insertions, 8 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index 303d27d355..1a27aa9f6a 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -51,7 +51,10 @@ type mutual_inductive_entry = {
   mind_entry_inds : one_inductive_entry list;
   mind_entry_polymorphic : bool; 
   mind_entry_universes : Univ.universe_context;
-  mind_entry_private : bool option }
+  mind_entry_private : bool option;
+  mind_entry_check_positivity : bool;
+  (** [false] if positivity is to be assumed. *)
+}
 
 (** {6 Constants (Definition/Axiom) } *)
 type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 72b615cc89..620c0f6d80 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -752,7 +752,7 @@ let compute_projections ((kn, _ as ind), u as indsp) 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 params kn isrecord isfinite inds nmr recargs =
+let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr recargs is_checked =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps = used_section_variables env inds in
@@ -857,7 +857,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
       mind_polymorphic = p;
       mind_universes = ctx;
       mind_private = prv;
-      mind_checked_positive = true;
+      mind_checked_positive = is_checked;
     }
 
 (************************************************************************)
@@ -872,4 +872,4 @@ let check_inductive env kn mie =
     build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
       env_ar params kn mie.mind_entry_record mie.mind_entry_finite
-      inds nmr recargs
+      inds nmr recargs mie.mind_entry_check_positivity
diff --git a/library/declare.ml b/library/declare.ml
index c3181e4c75..02e6daddeb 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -366,7 +366,8 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
   mind_entry_universes = Univ.UContext.empty;
-  mind_entry_private = None })
+  mind_entry_private = None;
+  mind_entry_check_positivity = true; })
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1b396d57ba..49bd37c697 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -553,7 +553,8 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_inds = entries;
     mind_entry_polymorphic = poly;
     mind_entry_private = if prv then Some false else None;
-    mind_entry_universes = Evd.universe_context evd },
+    mind_entry_universes = Evd.universe_context evd;
+    mind_entry_check_positivity = true; },
     impls
 
 (* Very syntactical equality *)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 7d5d61fb8b..df4f77fa19 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -115,5 +115,6 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
     mind_entry_inds = inds';
     mind_entry_polymorphic = mib.mind_polymorphic;
     mind_entry_private = mib.mind_private;
-    mind_entry_universes = univs
+    mind_entry_universes = univs;
+    mind_entry_check_positivity = mib.mind_checked_positive;
   }
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 737b7fb59f..2f7215adf8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -365,7 +365,8 @@ let declare_structure finite poly ctx id idbuild paramimpls params arity templat
       mind_entry_inds = [mie_ind];
       mind_entry_polymorphic = poly;
       mind_entry_private = None;
-      mind_entry_universes = ctx } in
+      mind_entry_universes = ctx;
+      mind_entry_check_positivity = true; } in
   let kn = Command.declare_mutual_inductive_with_eliminations mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in