From 090fffa57b2235f70d4355f5dc85d73fa2634655 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 17 Nov 2014 18:09:48 +0100
Subject: Option -type-in-type continued (deactivate test for inferred sort of
 inductive types + deactivate test for equality of sort + deactivate the check
 that the constraints Prop/Set <= Type are declared).

---
 kernel/indtypes.ml  | 6 +++---
 kernel/reduction.ml | 5 +++--
 2 files changed, 6 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 45e0261d3c..afd7cde979 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -299,8 +299,8 @@ let typecheck_inductive env ctx mie =
       let full_polymorphic () = 
 	let defu = Term.univ_of_sort def_level in
 	let is_natural =
-	  check_leq (universes env') infu defu && 
-	    not (is_type0m_univ defu && not is_unit)
+	  type_in_type env || (check_leq (universes env') infu defu &&
+	    not (is_type0m_univ defu && not is_unit))
 	in
 	let _ =
 	  (** Impredicative sort, always allow *)
@@ -326,7 +326,7 @@ let typecheck_inductive env ctx mie =
 	    (* conclusions of the parameters *)
             (* We enforce [u >= lev] in case [lev] has a strict upper *)
             (* constraints over [u] *)
-	    let b = check_leq (universes env') infu u in
+	    let b = type_in_type env || check_leq (universes env') infu u in
 	      if not b then
 		anomaly ~label:"check_inductive" 
 		  (Pp.str"Incorrect universe " ++
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 64964f85e8..704b345bdd 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -573,13 +573,14 @@ let check_sort_cmp_universes env pb s0 s1 univs =
       end
     | (Prop c1, Prop c2) -> if c1 != c2 then raise NotConvertible
     | (Prop c1, Type u) ->
-      let u0 = univ_of_sort s0 in
+	if not (type_in_type env) then
+	let u0 = univ_of_sort s0 in
 	(match pb with
 	| CUMUL -> check_leq univs u0 u
 	| CONV -> check_eq univs u0 u)
     | (Type u, Prop c) -> raise NotConvertible
     | (Type u1, Type u2) ->
-        if not (type_in_type env) then 
+        if not (type_in_type env) then
 	(match pb with
 	| CUMUL -> check_leq univs u1 u2
 	| CONV -> check_eq univs u1 u2)
-- 
cgit v1.2.3