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

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 28f7e69cd4..5caf052ace 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -16,6 +16,7 @@ open Context.Rel.Declaration
 
 let safe_flags = {
   check_guarded = true;
+  check_universes = true;
 }
 
 (** {6 Arities } *)
@@ -261,6 +262,7 @@ let subst_mind_body sub mib =
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private;
     mind_checked_positive = mib.mind_checked_positive;
+    mind_unsafe_universes = mib.mind_unsafe_universes;
   }
 
 let inductive_instance mib =
-- 
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/declareops.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 5caf052ace..211e5e062a 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -261,8 +261,7 @@ let subst_mind_body sub mib =
     mind_polymorphic = mib.mind_polymorphic;
     mind_universes = mib.mind_universes;
     mind_private = mib.mind_private;
-    mind_checked_positive = mib.mind_checked_positive;
-    mind_unsafe_universes = mib.mind_unsafe_universes;
+    mind_typing_flags = mib.mind_typing_flags;
   }
 
 let inductive_instance mib =
-- 
cgit v1.2.3