From 575da16f72ac125ba7e50b1bfe63302dee639973 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 13 May 2016 18:19:15 +0200
Subject: Adding a local type-in-type flag in kernel declarations.

---
 kernel/declarations.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 8b42a90e48..639cd061bc 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -73,6 +73,7 @@ type constant_universes = Univ.universe_context
 type typing_flags = {
   check_guarded : bool; (** If [false] then fixed points and co-fixed
                             points are assumed to be total. *)
+  check_universes : bool; (** If [false] universe constraints are not checked *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
@@ -192,6 +193,9 @@ type mutual_inductive_body = {
     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 *)
+
 }
 
 (** {6 Module declarations } *)
-- 
cgit v1.2.3


From 53ced0735f7e24735d78a02fc74588b8d9186eab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 17 Jun 2016 18:25:02 +0200
Subject: Moving the typing_flags to the environment.

---
 kernel/declarations.mli | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 639cd061bc..ef4d398c1f 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,9 +14,8 @@ open Term
    inductive definitions, modules and module types *)
 
 type set_predicativity = ImpredicativeSet | PredicativeSet
-type type_hierarchy = TypeInType | StratifiedType
 
-type engagement = set_predicativity * type_hierarchy
+type engagement = set_predicativity
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
-- 
cgit v1.2.3


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