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.
---
 library/declare.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'library')

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