Merge PR# 169: Local type-in-type flag.

1 files changed, 13 insertions, 5 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index d8493d9baf..9fb3bf79f6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -45,16 +45,15 @@ 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 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
@@ -211,6 +210,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
@@ -328,6 +330,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 +362,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 =
+  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 
   | TemplateArity _ -> true