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).

8 files changed, 18 insertions, 13 deletions

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)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 799ca25233..0dc7961103 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -711,7 +711,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	    (try
 	       let evd' =
 		 if pbty == CONV
-		 then Evd.set_eq_sort evd s1 s2
+		 then Evd.set_eq_sort env evd s1 s2
 		 else Evd.set_leq_sort env evd s1 s2
 	       in Success evd'
 	     with Univ.UniverseInconsistency p ->
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index d36a6a20fb..d5e3c6715c 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1114,12 +1114,16 @@ let normalize_sort evars s =
     if u' == u then s else Type u'
 
 (* FIXME inefficient *)
-let set_eq_sort d s1 s2 =
+let set_eq_sort env d s1 s2 =
   let s1 = normalize_sort d s1 and s2 = normalize_sort d s2 in
   match is_eq_sort s1 s2 with
   | None -> d
-  | Some (u1, u2) -> add_universe_constraints d 
-    (Universes.Constraints.singleton (u1,Universes.UEq,u2))
+  | Some (u1, u2) ->
+    if not (type_in_type env) then
+      add_universe_constraints d
+        (Universes.Constraints.singleton (u1,Universes.UEq,u2))
+    else
+      d
 
 let has_lub evd u1 u2 =
   (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 6c7ef2168c..df5269d345 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -504,7 +504,7 @@ val normalize_universe : evar_map -> Univ.universe -> Univ.universe
 val normalize_universe_instance : evar_map -> Univ.universe_instance -> Univ.universe_instance
 
 val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map
-val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
+val set_eq_sort : env -> evar_map -> sorts -> sorts -> evar_map
 val has_lub : evar_map -> Univ.universe -> Univ.universe -> evar_map
 val set_eq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
 val set_leq_level : evar_map -> Univ.universe_level -> Univ.universe_level -> evar_map
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index d566dd9b23..c1ac0d995b 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -520,7 +520,7 @@ let weaken_sort_scheme env evd set sort npars term ty =
       | Prod (n,t,c) ->
 	  if Int.equal np 0 then
             let osort, t' = change_sort_arity sort t in
-	      evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort env) !evdref sort osort;
+	      evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) env !evdref sort osort;
               mkProd (n, t', c),
               mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
 	  else
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3837ef0c8f..3e549fa846 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1267,7 +1267,7 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
 
 let sigma_compare_sorts env pb s0 s1 sigma =
   match pb with
-  | Reduction.CONV -> Evd.set_eq_sort sigma s0 s1
+  | Reduction.CONV -> Evd.set_eq_sort env sigma s0 s1
   | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1
     
 let sigma_compare_instances flex i0 i1 sigma =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f52f0f89b4..a59aceb8cf 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -654,7 +654,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
 	       let sigma' = 
 		 if pb == CUMUL
 		 then Evd.set_leq_sort curenv sigma s1 s2 
-		 else Evd.set_eq_sort sigma s1 s2 
+		 else Evd.set_eq_sort curenv sigma s1 s2
 	       in (sigma', metasubst, evarsubst)
 	     with e when Errors.noncritical e ->
                error_cannot_unify curenv sigma (m,n))