From 9a1e80524e1650311b019fedbd7e774242d80ea4 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 23 Jun 2015 09:24:43 +0200
Subject: 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.
---
 kernel/entries.mli | 5 ++++-
 kernel/indtypes.ml | 6 +++---
 2 files changed, 7 insertions(+), 4 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3