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