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/declarations.mli | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index ef4d398c1f..f89773fcc5 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -190,11 +190,8 @@ type mutual_inductive_body = {
     mind_universes : Univ.universe_context; (** Local universe variables and constraints *)
 
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
-  
-    mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker.  *)
-
-    mind_unsafe_universes : bool; (** generated with the type-in-type flag *)
 
+    mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)
 }
 
 (** {6 Module declarations } *)
-- 
cgit v1.2.3