From e759333a8b5c11247c4cc134fdde8c1bd85a6e17 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 11 Sep 2015 18:07:39 +0200
Subject: Universes: enforce Set <= i for all Type occurrences.

---
 kernel/indtypes.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel/indtypes.ml')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 8c89abe940..9c065101a3 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -286,7 +286,10 @@ let typecheck_inductive env mie =
 	let defu = Term.univ_of_sort def_level in
 	let is_natural =
 	  type_in_type env || (check_leq (universes env') infu defu &&
-	    not (is_type0m_univ defu && not is_unit))
+				not (is_type0m_univ defu && not is_unit)
+				  (* (~ is_type0m_univ defu \/ is_unit) (\* infu <= defu && not prop or unital *\) *)
+
+			     )
 	in
 	let _ =
 	  (** Impredicative sort, always allow *)
-- 
cgit v1.2.3