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

---
 kernel/entries.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'kernel/entries.mli')

diff --git a/kernel/entries.mli b/kernel/entries.mli
index 8b29e3abd7..df2c4653f7 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -52,8 +52,6 @@ type mutual_inductive_entry = {
   mind_entry_polymorphic : bool; 
   mind_entry_universes : Univ.universe_context;
   mind_entry_private : bool option;
-  mind_entry_check_positivity : bool;
-  (** [false] if positivity is to be assumed. *)
 }
 
 (** {6 Constants (Definition/Axiom) } *)
-- 
cgit v1.2.3