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/indTyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/indTyping.ml')

diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 179353d3f0..b2520b780f 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -77,7 +77,7 @@ let check_univ_leq ?(is_real_arg=false) env u info =
     else info
   in
   (* Inductive types provide explicit lifting from SProp to other universes, so allow SProp <= any. *)
-  if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
+  if Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
   then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
   else if is_impredicative_univ env ind_univ
        && Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
-- 
cgit v1.2.3