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

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index d8493d9baf..032e713593 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -328,6 +328,9 @@ let polymorphic_pconstant (cst,u) env =
   if Univ.Instance.is_empty u then false
   else polymorphic_constant cst env
 
+let type_in_type_constant cst env =
+  not (lookup_constant cst env).const_typing_flags.check_universes
+
 let template_polymorphic_constant cst env =
   match (lookup_constant cst env).const_type with 
   | TemplateArity _ -> true
@@ -357,6 +360,9 @@ let polymorphic_pind (ind,u) env =
   if Univ.Instance.is_empty u then false
   else polymorphic_ind ind env
 
+let type_in_type_ind (mind,i) env =
+  (lookup_mind mind env).mind_unsafe_universes
+
 let template_polymorphic_ind (mind,i) env =
   match (lookup_mind mind env).mind_packets.(i).mind_arity with 
   | TemplateArity _ -> true
-- 
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/environ.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 032e713593..65aaa3f7b3 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -45,16 +45,14 @@ let empty_named_context_val = empty_named_context_val
 let empty_env = empty_env
 
 let engagement env = env.env_stratification.env_engagement
+let typing_flags env = env.env_typing_flags
 
 let is_impredicative_set env = 
-  match fst (engagement env) with
+  match engagement env with
   | ImpredicativeSet -> true
   | _ -> false
 
-let type_in_type env =
-  match snd (engagement env) with
-  | TypeInType -> true
-  | _ -> false
+let type_in_type env = not (typing_flags env).check_universes
 
 let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context
@@ -211,6 +209,9 @@ let set_engagement c env = (* Unsafe *)
   { env with env_stratification =
     { env.env_stratification with env_engagement = c } }
 
+let set_typing_flags c env = (* Unsafe *)
+  { env with env_typing_flags = c }
+
 (* Global constants *)
 
 let lookup_constant = lookup_constant
-- 
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/environ.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 65aaa3f7b3..9fb3bf79f6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -53,6 +53,7 @@ let is_impredicative_set env =
   | _ -> false
 
 let type_in_type env = not (typing_flags env).check_universes
+let deactivated_guard env = not (typing_flags env).check_guarded
 
 let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context
@@ -362,7 +363,7 @@ let polymorphic_pind (ind,u) env =
   else polymorphic_ind ind env
 
 let type_in_type_ind (mind,i) env =
-  (lookup_mind mind env).mind_unsafe_universes
+  not (lookup_mind mind env).mind_typing_flags.check_universes
 
 let template_polymorphic_ind (mind,i) env =
   match (lookup_mind mind env).mind_packets.(i).mind_arity with 
-- 
cgit v1.2.3