Providing a -type-in-type option for collapsing the universe hierarchy.

15 files changed, 22 insertions, 22 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 567078f85..726e64e81 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1733,7 +1733,7 @@ let build_inversion_problem loc env sigma tms t =
   (* let sigma, s = Evd.new_sort_variable univ_flexible sigma in *)
   let s' = Retyping.get_sort_of env sigma t in
   let sigma, s = Evd.new_sort_variable univ_flexible_alg sigma in
-  let sigma = Evd.set_leq_sort sigma s' s in
+  let sigma = Evd.set_leq_sort env sigma s' s in
   let evdref = ref sigma in
   (* let ty = evd_comb1 (refresh_universes false) evdref ty in *)
   let pb =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index a1279c1f2..6a48d84ed 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -403,7 +403,7 @@ let inh_coerce_to_sort loc env evd j =
     match kind_of_term typ with
     | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
     | Evar ev when not (is_defined evd (fst ev)) ->
-	let (evd',s) = define_evar_as_sort evd ev in
+	let (evd',s) = define_evar_as_sort env evd ev in
 	  (evd',{ utj_val = j.uj_val; utj_type = s })
     | _ ->
 	inh_tosort_force loc env evd j
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d125a799b..47955e8e0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -679,7 +679,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	       let evd' =
 		 if pbty == CONV
 		 then Evd.set_eq_sort evd s1 s2
-		 else Evd.set_leq_sort evd s1 s2
+		 else Evd.set_leq_sort env evd s1 s2
 	       in Success evd'
 	     with Univ.UniverseInconsistency p ->
                UnifFailure (evd,UnifUnivInconsistency p)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 631438ddf..f32238ee7 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -59,8 +59,8 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
     let status = if inferred then Evd.univ_flexible_alg else Evd.univ_flexible in
     let s' = evd_comb0 (new_sort_variable status) evdref in
     let evd = 
-      if dir then set_leq_sort !evdref s' s
-      else set_leq_sort !evdref s s'
+      if dir then set_leq_sort env !evdref s' s
+      else set_leq_sort env !evdref s s'
     in
       modified := true; evdref := evd; mkSort s'
     | Prod (na,u,v) -> 
@@ -1154,7 +1154,7 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
 	      ~src:evi.evar_source ~filter:evi.evar_filter 
 	      ?candidates:evi.evar_candidates (it_mkProd_or_LetIn (mkSort k) ctx) 
 	  in
-	  let evd = Evd.set_leq_sort (Evd.set_leq_sort evd k i) k j in
+	  let evd = Evd.set_leq_sort env (Evd.set_leq_sort env evd k i) k j in
 	  let evd = solve_evar_evar ~force f g env evd (Some false) (ev3,args1) ev1 in
 	    f env evd pbty ev2 (whd_evar evd (mkEvar (ev3,args1)))
     with Reduction.NotArity -> 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ddc1ece96..d9e9ac8f9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -716,7 +716,7 @@ let define_pure_evar_as_product evd evk =
 	let evd3, (rng, srng) =
 	  new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in
 	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
-	let evd3 = Evd.set_leq_sort evd3 (Type prods) s in
+	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
 	  evd3, rng
   in
   let prod = mkProd (Name id, dom, subst_var id rng) in
@@ -780,12 +780,12 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function
 
 (* Refining an evar to a sort *)
 
-let define_evar_as_sort evd (ev,args) =
+let define_evar_as_sort env evd (ev,args) =
   let evd, u = new_univ_variable univ_rigid evd in
   let evi = Evd.find_undefined evd ev in 
   let s = Type u in
   let evd' = Evd.define ev (mkSort s) evd in
-    Evd.set_leq_sort evd' (Type (Univ.super u)) (destSort evi.evar_concl), s
+    Evd.set_leq_sort env evd' (Type (Univ.super u)) (destSort evi.evar_concl), s
 
 (* We don't try to guess in which sort the type should be defined, since
    any type has type Type. May cause some trouble, but not so far... *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 081c41560..b90a78434 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -92,7 +92,7 @@ val check_evars : env -> evar_map -> evar_map -> constr -> unit
 
 val define_evar_as_product : evar_map -> existential -> evar_map * types
 val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
-val define_evar_as_sort : evar_map -> existential -> evar_map * sorts
+val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
 
 (** Instantiate an evar by as many lambda's as needed so that its arguments
     are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 813a21229..c4bf366ac 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1193,7 +1193,7 @@ let set_eq_instances ?(flex=false) d u1 u2 =
   add_universe_constraints d
     (Universes.enforce_eq_instances_univs flex u1 u2 Universes.Constraints.empty)
 
-let set_leq_sort evd s1 s2 =
+let set_leq_sort env evd s1 s2 =
   let s1 = normalize_sort evd s1 
   and s2 = normalize_sort evd s2 in
   match is_eq_sort s1 s2 with
@@ -1205,7 +1205,9 @@ let set_leq_sort evd s1 s2 =
     (* else if Univ.is_type0m_univ u2 then  *)
     (*   raise (Univ.UniverseInconsistency (Univ.Le, u1, u2, [])) *)
     (* else  *)
+      if not (type_in_type env) then
       add_universe_constraints evd (Universes.Constraints.singleton (u1,Universes.ULe,u2))
+      else evd
 	    
 let check_eq evd s s' =
   Univ.check_eq evd.universes.uctx_universes s s'
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 12a166e66..be8ca7cd5 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -273,8 +273,6 @@ val drop_side_effects : evar_map -> evar_map
     point. This section defines the relevant manipulation functions. *)
 
 val whd_sort_variable : evar_map -> constr -> constr
-val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
-val set_eq_sort : evar_map -> sorts -> sorts -> evar_map
 
 exception UniversesDiffer
 
@@ -462,7 +460,7 @@ val whd_sort_variable : evar_map -> constr -> constr
 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 : evar_map -> sorts -> sorts -> evar_map
+val set_leq_sort : env -> evar_map -> sorts -> sorts -> evar_map
 val set_eq_sort : 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
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0cbfa7597..9f460d08f 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -517,7 +517,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) !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/inductiveops.ml b/pretyping/inductiveops.ml
index 4b6107c4e..24bf7cbc0 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -557,7 +557,7 @@ let rec instantiate_universes env evdref scl is = function
         else
           (* unconstrained sort: replace by fresh universe *)
           let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in
-	  let evm = Evd.set_leq_sort evm s (Sorts.sort_of_univ u) in
+	  let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in
 	    evdref := evm; s
       in
       (na,None,mkArity(ctx,s)):: instantiate_universes env evdref scl is (sign, exp)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 28ab88526..ad6a79863 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -953,7 +953,7 @@ and pretype_type resolve_tc valcon env evdref lvar = function
 	       match kind_of_term (whd_betadeltaiota env sigma t) with
                | Sort s -> s
                | Evar ev when is_Type (existential_type sigma ev) ->
-		   evd_comb1 (define_evar_as_sort) evdref ev
+		   evd_comb1 (define_evar_as_sort env) evdref ev
                | _ -> anomaly (Pp.str "Found a type constraint which is not a type")
            in
 	     { utj_val = v;
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 025725934..10f2bfd5b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1233,10 +1233,10 @@ let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y
     | Univ.UniverseInconsistency _ -> false
     | e when is_anomaly e -> error "Conversion test raised an anomaly"
 
-let sigma_compare_sorts pb s0 s1 sigma =
+let sigma_compare_sorts env pb s0 s1 sigma =
   match pb with
   | Reduction.CONV -> Evd.set_eq_sort sigma s0 s1
-  | Reduction.CUMUL -> Evd.set_leq_sort sigma s0 s1
+  | Reduction.CUMUL -> Evd.set_leq_sort env sigma s0 s1
     
 let sigma_compare_instances flex i0 i1 sigma =
   try Evd.set_eq_instances ~flex sigma i0 i1
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index aedb41037..6672c7fa7 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -250,7 +250,7 @@ type conversion_test = constraints -> constraints
 val pb_is_equal : conv_pb -> bool
 val pb_equal : conv_pb -> conv_pb
 
-val sort_cmp : conv_pb -> sorts -> sorts -> universes -> unit
+val sort_cmp : env -> conv_pb -> sorts -> sorts -> universes -> unit
 
 val is_conv : env ->  evar_map -> constr -> constr -> bool
 val is_conv_leq : env ->  evar_map -> constr -> constr -> bool
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 1485b7701..eafc5da9a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -38,7 +38,7 @@ let e_type_judgment env evdref j =
   match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
-        let (evd,s) = Evarutil.define_evar_as_sort !evdref ev in
+        let (evd,s) = Evarutil.define_evar_as_sort env !evdref ev in
         evdref := evd; { utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_type env j
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 124faf05b..b07bf4f92 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -588,7 +588,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	    (try 
 	       let sigma' = 
 		 if pb == CUMUL
-		 then Evd.set_leq_sort sigma s1 s2 
+		 then Evd.set_leq_sort env sigma s1 s2 
 		 else Evd.set_eq_sort sigma s1 s2 
 	       in (sigma', metasubst, evarsubst)
 	     with e when Errors.noncritical e ->