From 316592a31b463568f5136757c3570eaa8e1f0167 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 25 Sep 2020 15:31:51 +0200
Subject: Put type-in-type flag in ugraph.

Fix #13086.
---
 kernel/environ.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'kernel/environ.ml')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 03c9cb4be6..e497b7904a 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -467,14 +467,22 @@ let same_flags {
 [@warning "+9"]
 
 let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b)
+let set_type_in_type b = map_universes (UGraph.set_type_in_type b)
 
 let set_typing_flags c env =
   if same_flags env.env_typing_flags c then env
-  else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c }
+  else
+    let env = { env with env_typing_flags = c } in
+    let env = set_cumulative_sprop c.cumulative_sprop env in
+    let env = set_type_in_type (not c.check_universes) env in
+    env
 
 let set_cumulative_sprop b env =
   set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
 
+let set_type_in_type b env =
+  set_typing_flags {env.env_typing_flags with check_universes=not b} env
+
 let set_allow_sprop b env =
   { env with env_stratification =
     { env.env_stratification with env_sprop_allowed = b } }
-- 
cgit v1.2.3