From ecb032467557631ea60324c6afa55c91c133e40d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 17 Jun 2016 20:26:35 +0200
Subject: Reuse the typing_flags datatype for inductives.

---
 library/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 4e9e68dff..f809e9742 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -354,7 +354,7 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_polymorphic = false;
   mind_entry_universes = Univ.UContext.empty;
   mind_entry_private = None;
-  mind_entry_check_positivity = true; })
+})
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
-- 
cgit v1.2.3