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 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel/entries.mli')

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