From 53ced0735f7e24735d78a02fc74588b8d9186eab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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 032e71359..65aaa3f7b 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