Tentative to make unification check types at every instanciation of an

evar, and simultaneously make type inference with universes work better.
This only exports more functions from kernel/univ, to be able to work
with a set of universe variables during type inference. Universe
constraints are gradually added during type checking, adding information
necessary e.g. to lower the level of unknown Type variables to Prop or
Set. There does not seem to be a disastrous performance hit on the
stdlib, but might have one on some contribs (hence the "Tentative").


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 167 insertions, 97 deletions

diff --git a/kernel/univ.ml b/kernel/univ.ml
index e31e2be689..660e39e637 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -54,6 +54,11 @@ module UniverseLevel = struct
 end
 
 module UniverseLMap = Map.Make (UniverseLevel)
+module UniverseLSet = Set.Make (UniverseLevel)
+
+type universe_level = UniverseLevel.t
+
+let compare_levels = UniverseLevel.compare
 
 (* An algebraic universe [universe] is either a universe variable
    [UniverseLevel.t] or a formal universe known to be greater than some
@@ -71,7 +76,13 @@ type universe =
   | Atom of UniverseLevel.t
   | Max of UniverseLevel.t list * UniverseLevel.t list
 
-let make_univ (m,n) = Atom (UniverseLevel.Level (m,n))
+let make_universe_level (m,n) = UniverseLevel.Level (m,n)
+let make_universe l = Atom l
+let make_univ c = Atom (make_universe_level c)
+
+let universe_level = function
+  | Atom l -> Some l
+  | Max _ -> None
 
 let pr_uni_level u = str (UniverseLevel.to_string u)
 
@@ -500,9 +511,6 @@ let merge_constraints c g =
 
 (* Normalization *)
 
-module UniverseLSet =
- Set.Make (UniverseLevel)
-
 let lookup_level u g =
   try Some (UniverseLMap.find u g) with Not_found -> None
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e19a4c43a7..2f99e16ec7 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -8,8 +8,11 @@
 
 (** Universes. *)
 
+type universe_level
 type universe
 
+module UniverseLSet : Set.S with type elt = universe_level
+
 (** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... 
    Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *)
 
@@ -17,12 +20,17 @@ val type0m_univ : universe  (** image of Prop in the universes hierarchy *)
 val type0_univ : universe  (** image of Set in the universes hierarchy *)
 val type1_univ : universe  (** the universe of the type of Prop/Set *)
 
+val make_universe_level : Names.dir_path * int -> universe_level
+val make_universe : universe_level -> universe
 val make_univ : Names.dir_path * int -> universe
 
 val is_type0_univ : universe -> bool
 val is_type0m_univ : universe -> bool
 val is_univ_variable : universe -> bool
 
+val universe_level : universe -> universe_level option
+val compare_levels : universe_level -> universe_level -> int
+
 (** The type of a universe *)
 val super : universe -> universe
 
@@ -82,6 +90,7 @@ val no_upper_constraints : universe -> constraints -> bool
 
 (** {6 Pretty-printing of universes. } *)
 
+val pr_uni_level : universe_level -> Pp.std_ppcmds
 val pr_uni : universe -> Pp.std_ppcmds
 val pr_universes : universes -> Pp.std_ppcmds
 val pr_constraints : constraints -> Pp.std_ppcmds
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 28bf6e64d0..509a4e9e5f 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -159,9 +159,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
     let c = constr_of_global ref in
       make_judge c (Retyping.get_type_of env Evd.empty c)
 
-  let pretype_sort = function
+  let pretype_sort evdref = function
     | GProp c -> judge_of_prop_contents c
-    | GType _ -> judge_of_new_Type ()
+    | GType _ -> evd_comb0 judge_of_new_Type evdref
 
   let split_tycon_lam loc env evd tycon =
     let rec real_split evd c =
@@ -307,7 +307,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
     | GSort (loc,s) ->
-	inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
+	let s' = pretype_sort evdref s in
+	inh_conv_coerce_to_tycon loc env evdref s' tycon
 
     | GApp (loc,f,args) ->
 	let length = List.length args in
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8e0d28fbfb..5e2c0729c8 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -948,7 +948,7 @@ let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl =
 let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
   let pred= abstract_predicate env !evdref indf current dep tms p in
   (pred, whd_betaiota !evdref
-           (applist (pred, realargs@[current])), new_Type ())
+           (applist (pred, realargs@[current])))
 
 let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb =
   match typ, oldtyp with
@@ -1164,7 +1164,7 @@ and match_current pb tomatch =
 
 	  (* We build the (elementary) case analysis *)
 	  let brvals = Array.map (fun (v,_) -> v) brs in
-	  let (pred,typ,s) =
+	  let (pred,typ) =
 	    find_predicate pb.caseloc pb.env pb.evdref
 	      pb.pred current indt (names,dep) pb.tomatch in
 	  let ci = make_case_info pb.env mind pb.casestyle in
@@ -1621,7 +1621,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs sign tycon pred =
 	(* we use two strategies *)
         let sigma,t = match tycon with
 	| Some (None, t) -> sigma,t
-	| _ -> new_evar sigma env ~src:(loc, CasesType) (new_Type ()) in
+	| _ -> new_type_evar sigma env ~src:(loc, CasesType) in
         (* First strategy: we build an "inversion" predicate *)
 	let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
 	(* Second strategy: we directly use the evar as a non dependent pred *)
@@ -1631,8 +1631,9 @@ let prepare_predicate loc typing_fun sigma env tomatchs sign tycon pred =
     | Some rtntyp, _ ->
       (* We extract the signature of the arity *)
       let env = List.fold_right push_rels arsign env in
+      let sigma, newt = new_sort_variable sigma in
       let evdref = ref sigma in
-      let predcclj = typing_fun (mk_tycon (new_Type ())) env evdref rtntyp in
+      let predcclj = typing_fun (mk_tycon (mkSort newt)) env evdref rtntyp in
       let sigma = Option.cata (fun tycon ->
           let tycon = lift_tycon_type (List.length arsign) tycon in
           Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3906f87288..c5bcb631e7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -26,28 +26,33 @@ type flex_kind_of_term =
   | MaybeFlexible of constr (* approx'ed as reducible but not necessarily so *)
   | Flexible of existential
 
-let flex_kind_of_term ts c l =
+let flex_kind_of_term c l =
   match kind_of_term c with
-    | Const n when is_transparent_constant ts n -> MaybeFlexible c
-    | Rel n -> MaybeFlexible c
-    | Var id when is_transparent_variable ts id -> MaybeFlexible c
+    | Rel _ | Const _ | Var _ -> MaybeFlexible c
     | Lambda _ when l<>[] -> MaybeFlexible c
     | LetIn _  -> MaybeFlexible c
     | Evar ev -> Flexible ev
     | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ -> Rigid c
-    | Meta _ | Case _ | Fix _ | Const _ | Var _ -> PseudoRigid c
+    | Meta _ | Case _ | Fix _ -> PseudoRigid c
     | Cast _ | App _ -> assert false
 
 let is_rigid = function Rigid _ -> true | _ -> false
 
-let eval_flexible_term env c =
+let eval_flexible_term ts env c =
   match kind_of_term c with
-  | Const c -> constant_opt_value env c
+  | Const c -> 
+      if is_transparent_constant ts c
+      then constant_opt_value env c
+      else None
   | Rel n ->
       (try let (_,v,_) = lookup_rel n env in Option.map (lift n) v
       with Not_found -> None)
   | Var id ->
-      (try let (_,v,_) = lookup_named id env in v with Not_found -> None)
+      (try
+	 if is_transparent_variable ts id then
+	   let (_,v,_) = lookup_named id env in v 
+	 else None 
+       with Not_found -> None)
   | LetIn (_,b,_,c) -> Some (subst1 b c)
   | Lambda _ -> Some c
   | _ -> assert false
@@ -194,7 +199,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
 
 and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
   (* Evar must be undefined since we have flushed evars *)
-  match (flex_kind_of_term ts term1 l1, flex_kind_of_term ts term2 l2) with
+  match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with
 
     | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
 	let f1 i =
@@ -249,7 +254,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                (fun i -> evar_conv_x ts env i pbty term1 (applist(term2,deb2)))]
           else (i,false)
 	and f2 i =
-	  match eval_flexible_term env flex2 with
+	  match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
 		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None -> (i,false)
@@ -281,7 +286,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
                (fun i -> evar_conv_x ts env i pbty (applist(term1,deb1)) term2)]
           else (i,false)
 	and f2 i =
-	  match eval_flexible_term env flex1 with
+	  match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
 		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
 	    | None -> (i,false)
@@ -324,20 +329,20 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
              usable as a canonical projection *)
 	  if isLambda flex1 or is_open_canonical_projection i appr2
 	  then
-	    match eval_flexible_term env flex1 with
+	    match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
 		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
 	    | None ->
-		match eval_flexible_term env flex2 with
+		match eval_flexible_term ts env flex2 with
 		| Some v2 ->
 		    evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
 		| None -> (i,false)
 	  else
-	    match eval_flexible_term env flex2 with
+	    match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
 		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None ->
-		match eval_flexible_term env flex1 with
+		match eval_flexible_term ts env flex1 with
 		| Some v1 ->
 		    evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
 		| None -> (i,false)
@@ -411,7 +416,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  (try conv_record ts env i (check_conv_record appr1 appr2)
            with Not_found -> (i,false))
 	and f4 i =
-	  match eval_flexible_term env flex1 with
+	  match eval_flexible_term ts env flex1 with
 	    | Some v1 ->
  		evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
 	    | None -> (i,false)
@@ -423,7 +428,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  (try conv_record ts env i (check_conv_record appr2 appr1)
            with Not_found -> (i,false))
 	and f4 i =
-	  match eval_flexible_term env flex2 with
+	  match eval_flexible_term ts env flex2 with
 	    | Some v2 ->
  		evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
 	    | None -> (i,false)
@@ -434,7 +439,14 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
         match kind_of_term c1, kind_of_term c2 with
 
 	| Sort s1, Sort s2 when l1=[] & l2=[] ->
-	    (evd, base_sort_cmp pbty s1 s2)
+	    (try 
+	       let evd' = 
+		 if pbty = CONV 
+		 then Evd.set_eq_sort evd s1 s2 
+		 else Evd.set_leq_sort evd s1 s2 
+	       in (evd', true)
+	     with Univ.UniverseInconsistency _ -> (evd, false)
+	     | _ -> (evd, false))
 
 	| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
             ise_and evd
@@ -508,7 +520,6 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
 	| (Lambda _ | Rel _ | Var _ | Const _ | Evar _), _ -> assert false
 	| _, (Lambda _ | Rel _ | Var _ | Const _ | Evar _) -> assert false
-
       end
 
     | PseudoRigid _, Rigid _ ->  (evd,false)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 418f683319..b88ea03e19 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1297,7 +1297,7 @@ let status_changed lev (pbty,_,t1,t2) =
 
 (* Util *)
 
-let check_instance_type conv_algo env evd ev1 t2 =
+let check_instance_type conv_algo pbty env evd ev1 t2 =
   let t2 = nf_evar evd t2 in
   if has_undefined_evars_or_sorts evd t2 then
     (* May contain larger constraints than needed: don't want to
@@ -1309,9 +1309,9 @@ let check_instance_type conv_algo env evd ev1 t2 =
     else
       let typ1 = existential_type evd ev1 in
       let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in
-      if b then evd else
-	user_err_loc (fst (evar_source (fst ev1) evd),"",
-	  str "Unable to find a well-typed instantiation")
+	if b then evd else
+	  user_err_loc (fst (evar_source (fst ev1) evd),"",
+			str "Unable to find a well-typed instantiation")
 
 (* Tries to solve problem t1 = t2.
  * Precondition: t1 is an uninstantiated evar
@@ -1334,11 +1334,7 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
 	    else
 	      add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
       | _ ->
-	  let evd =
-	    if pbty = Some false then
-	      check_instance_type conv_algo env evd ev1 t2
-	    else
-	      evd in
+	  let evd = check_instance_type conv_algo pbty env evd ev1 t2 in
 	  let evd = evar_define ~choose env ev1 t2 evd in
 	  let evi = Evd.find evd evk1 in
 	    if occur_existential evd evi.evar_concl then
@@ -1480,31 +1476,25 @@ let empty_valcon = None
 (* Builds a value constraint *)
 let mk_valcon c = Some c
 
-(* Refining an evar to a product
-
-   I.e., solve x1..xq |- ?e:T(x1..xq) with e:=Πy:?dom[x1..xq].?rng[x1..xq,y]
-   where x1..xq |- ?dom:Type and x1..xq,y |- ?rng:Type
 
-   Note: Declaring any type to be in the sort Type shouldn't be harmful
-   since cumulativity now includes Prop and Set in Type...
-   It is, but that's not too bad
-
-   To do: should we check that T is Type and instantiate it by a sort
-   if an evar?
-*)
+let new_type_evar ?src ?filter evd env =
+  let evd', s = new_sort_variable evd in
+    new_evar evd' env ?src ?filter (mkSort s)
 
 let idx = id_of_string "x"
 
+(* Refining an evar to a product *)
+
 let define_pure_evar_as_product evd evk =
   let evi = Evd.find_undefined evd evk in
   let evenv = evar_unfiltered_env evi in
   let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
-  let evd1,dom = new_evar evd evenv (new_Type()) ~filter:(evar_filter evi) in
+  let evd1,dom = new_type_evar evd evenv ~filter:(evar_filter evi) in
   let evd2,rng =
     let newenv = push_named (id, None, dom) evenv in
     let src = evar_source evk evd1 in
     let filter = true::evar_filter evi in
-    new_evar evd1 newenv ~src (new_Type()) ~filter in
+    new_type_evar evd1 newenv ~src ~filter in
   let prod = mkProd (Name id, dom, subst_var id rng) in
   let evd3 = Evd.define evk prod evd2 in
   evd3,prod
@@ -1558,13 +1548,15 @@ let define_evar_as_lambda env evd (evk,args) =
 (* Refining an evar to a sort *)
 
 let define_evar_as_sort evd (ev,args) =
-  let s = new_Type () in
-  Evd.define ev s evd, destSort s
+  let evd, s = new_sort_variable evd in
+    Evd.define ev (mkSort s) evd, 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... *)
 
-let judge_of_new_Type () = Typeops.judge_of_type (new_univ ())
+let judge_of_new_Type evd = 
+  let evd', s = new_univ_variable evd in
+    evd', Typeops.judge_of_type s
 
 (* Propagation of constraints through application and abstraction:
    Given a type constraint on a functional term, returns the type
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 3127d87eda..4d28d66e71 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -34,6 +34,11 @@ val new_evar :
 val e_new_evar :
   evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr
 
+(** Create a new Type existential variable, as we keep track of 
+    them during type-checking and unification. *)
+val new_type_evar :
+  ?src:loc * hole_kind -> ?filter:bool list -> evar_map -> env -> evar_map * constr
+
 (** Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
    [sign] and type [ty], [inst] is a mapping of the evar context to
@@ -114,7 +119,7 @@ val undefined_evars_of_evar_info : evar_map -> evar_info -> Intset.t
 
 (** {6 Value/Type constraints} *)
 
-val judge_of_new_Type : unit -> unsafe_judgment
+val judge_of_new_Type : evar_map -> evar_map * unsafe_judgment
 
 type type_constraint_type = (int * int) option * constr
 type type_constraint = type_constraint_type option
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index e5347b7f60..4e1795a978 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -210,8 +210,8 @@ module EvarInfoMap = struct
 end
 
 module EvarMap = struct
-  type t = EvarInfoMap.t * Univ.universes
-  let empty = EvarInfoMap.empty, Univ.initial_universes
+  type t = EvarInfoMap.t * (Univ.UniverseLSet.t * Univ.universes)
+  let empty = EvarInfoMap.empty, (Univ.UniverseLSet.empty, Univ.initial_universes)
   let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm)
   let add_undefined (sigma,sm) k v = (EvarInfoMap.add_undefined sigma k v, sm)
   let find (sigma,_) = EvarInfoMap.find sigma
@@ -237,8 +237,8 @@ module EvarMap = struct
         EvarInfoMap.is_defined sigma2 k))
 
   let merge e e' = fold e' (fun n v sigma -> add sigma n v) e
-  let add_constraints (sigma, sm) cstrs =
-    (sigma, Univ.merge_constraints cstrs sm)
+  let add_constraints (sigma, (us, sm)) cstrs =
+    (sigma, (us, Univ.merge_constraints cstrs sm))
 end
 
 (*******************************************************************)
@@ -391,7 +391,7 @@ let subst_evar_info s evi =
       evar_body = subst_evb evi.evar_body }
 
 let subst_evar_defs_light sub evd =
-  assert (Univ.initial_universes = (snd evd.evars));
+  assert (Univ.initial_universes = (snd (snd evd.evars)));
   assert (evd.conv_pbs = []);
   { evd with
       metas = Metamap.map (map_clb (subst_mps sub)) evd.metas;
@@ -490,11 +490,16 @@ let evar_list evd c =
 (**********************************************************)
 (* Sort variables *)
 
-let new_sort_variable ({ evars = (sigma,sm) } as d)=
-  let u = Termops.new_univ() in
-    (Type u, d)
+let new_univ_variable ({ evars = (sigma,(us,sm)) } as d) =
+  let u = Termops.new_univ_level () in
+  let us' = Univ.UniverseLSet.add u us in
+    ({d with evars = (sigma, (us', sm))}, Univ.make_universe u)
+  
+let new_sort_variable d =
+  let (d', u) = new_univ_variable d in
+    (d', Type u)
 
-let is_sort_variable {evars=(_,sm)} s = match s with Type _ -> true | _ -> false 
+let is_sort_variable {evars=(_,(us,_))} s = match s with Type u -> true | _ -> false 
 let whd_sort_variable {evars=(_,sm)} t = t
 
 let univ_of_sort = function
@@ -502,26 +507,56 @@ let univ_of_sort = function
   | Prop Pos -> Univ.type0_univ
   | Prop Null -> Univ.type0m_univ
 
-let set_leq_sort d s1 s2 =
-  if s1 = s2 then d
+let is_eq_sort s1 s2 =
+  if s1 = s2 then None
   else 
     let u1 = univ_of_sort s1 and u2 = univ_of_sort s2 in
+      if u1 = u2 then None
+      else Some (u1, u2)
+
+let is_univ_var_or_set u =   
+  Univ.is_univ_variable u || u = Univ.type0_univ
+
+let set_leq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
+  match is_eq_sort s1 s2 with
+  | None -> d
+  | Some (u1, u2) ->
       match s1, s2 with
       | Prop c, Prop c' -> 
 	  if c = Null && c' = Pos then d
 	  else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)))
-      | _, _ ->
-	  add_constraints d (Univ.enforce_geq u2 u1 Univ.empty_constraint)
-
-let set_eq_sort d s1 s2 =
-  if s1 = s2 then d
-  else
-    let u1, u2 = univ_of_sort s1, univ_of_sort s2 in
+     | Type u, Prop c -> 
+	  if c = Pos then 
+	    add_constraints d (Univ.enforce_geq Univ.type0_univ u Univ.empty_constraint)
+	  else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2))
+      | _, Type u ->
+	  if is_univ_var_or_set u then
+	    add_constraints d (Univ.enforce_geq u2 u1 Univ.empty_constraint)
+	  else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2))
+
+let is_univ_level_var us u =
+  match Univ.universe_level u with
+  | Some u -> Univ.UniverseLSet.mem u us
+  | None -> false
+
+let set_eq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 =
+  match is_eq_sort s1 s2 with
+  | None -> d
+  | Some (u1, u2) ->
       match s1, s2 with
-      | Prop c, Prop c' -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2))
-      | _, _ ->
+      | Prop c, Type u when is_univ_level_var us u ->
 	  add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
-
+      | Type u, Prop c when is_univ_level_var us u ->
+	  add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
+      | Type u, Type v when (is_univ_level_var us u) || (is_univ_level_var us v) ->
+	  add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
+      | Prop c, Type u when is_univ_var_or_set u &&
+	  Univ.check_eq sm u1 u2 -> d
+      | Type u, Prop c when is_univ_var_or_set u && Univ.check_eq sm u1 u2 -> d
+      | Type u, Type v when is_univ_var_or_set u && is_univ_var_or_set v ->
+	  add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint)
+      | _, _ -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2))
+	    
 (**********************************************************)
 (* Accessing metas *)
 
@@ -717,7 +752,7 @@ let pr_evar_info evi =
   in
   hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
 
-let pr_evar_map_t (evars,univs as sigma) =
+let pr_evar_map_t (evars,(uvs,univs) as sigma) =
   let evs =
     if evars = EvarInfoMap.empty then mt ()
     else
@@ -726,11 +761,16 @@ let pr_evar_map_t (evars,univs as sigma) =
 		(fun (ev,evi) ->
 		  h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
 		(EvarMap.to_list sigma))++fnl()
-  and cs =
+  and svs =
+    if Univ.UniverseLSet.is_empty uvs then mt ()
+    else str"UNIVERSE VARIABLES:"++brk(0,1)++
+      h 0 (prlist_with_sep pr_fnl 
+	     (fun u -> Univ.pr_uni_level u) (Univ.UniverseLSet.elements uvs))++fnl()
+   and cs =
     if univs = Univ.initial_universes then mt ()
     else str"UNIVERSES:"++brk(0,1)++
       h 0 (Univ.pr_universes univs)++fnl()
-  in evs ++ cs
+  in evs ++ svs ++ cs
 
 let pr_constraints pbs =
   h 0
@@ -749,8 +789,7 @@ let pr_evar_map evd =
   let pp_evm =
     if evd.evars = EvarMap.empty then mt() else
       pr_evar_map_t evd.evars++fnl() in
-  let cstrs =
-    if evd.conv_pbs = [] then mt() else
+  let cstrs = if evd.conv_pbs = [] then mt() else
     str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in
   let pp_met =
     if evd.metas = Metamap.empty then mt() else
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 29c505d92f..bb345580ee 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -247,7 +247,8 @@ val subst_defined_metas : metabinding list -> constr -> constr option
 (*********************************************************
    Sort variables *)
 
-val new_sort_variable : evar_map -> sorts * evar_map
+val new_univ_variable : evar_map -> evar_map * Univ.universe
+val new_sort_variable : evar_map -> evar_map * sorts
 val is_sort_variable : evar_map -> sorts -> bool
 val whd_sort_variable : evar_map -> constr -> constr
 val set_leq_sort : evar_map -> sorts -> sorts -> evar_map
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e3b8dbc204..aefa7dfd43 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -292,12 +292,15 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let c = constr_of_global ref in
       make_judge c (Retyping.get_type_of env Evd.empty c)
 
-  let pretype_sort = function
+  let pretype_sort evdref = function
     | GProp c -> judge_of_prop_contents c
-    | GType _ -> judge_of_new_Type ()
+    | GType _ -> evd_comb0 judge_of_new_Type evdref
 
   exception Found of fixpoint
 
+  let new_type_evar evdref env loc =
+    evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,InternalHole)) evdref
+
   (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
   (* in environment [env], with existential variables [evdref] and *)
   (* the type constraint tycon *)
@@ -327,8 +330,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	let ty =
           match tycon with
             | Some (None, ty) -> ty
-            | None | Some _ ->
-		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+            | None | Some _ -> new_type_evar evdref env loc in
         let k = MatchingVar (someta,n) in
 	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
@@ -337,7 +339,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
           match tycon with
             | Some (None, ty) -> ty
             | None | Some _ ->
-		e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ()) in
+		new_type_evar evdref env loc in
 	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
     | GRec (loc,fixkind,names,bl,lar,vdef) ->
@@ -404,7 +406,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	inh_conv_coerce_to_tycon loc env evdref fixj tycon
 
     | GSort (loc,s) ->
-	inh_conv_coerce_to_tycon loc env evdref (pretype_sort s) tycon
+	let j = pretype_sort evdref s in
+	  inh_conv_coerce_to_tycon loc env evdref j tycon
 
     | GApp (loc,f,args) ->
 	let fj = pretype empty_tycon env evdref lvar f in
@@ -547,9 +550,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		     let v =
 		       let mis,_ = dest_ind_family indf in
 		       let ci = make_case_info env mis LetStyle in
-			 mkCase (ci, p, cj.uj_val,[|f|] )
-		     in
-		       { uj_val = v; uj_type = ccl })
+			 mkCase (ci, p, cj.uj_val,[|f|])
+		     in { uj_val = v; uj_type = ccl })
 
     | GIf (loc,c,(na,po),b1,b2) ->
 	let cj = pretype empty_tycon env evdref lvar c in
@@ -586,8 +588,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	    | None ->
 		let p = match tycon with
 		  | Some (None, ty) -> ty
-		  | None | Some _ ->
-                      e_new_evar evdref env ~src:(loc,InternalHole) (new_Type ())
+		  | None | Some _ -> new_type_evar evdref env loc
 		in
 		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
 	  let pred = nf_evar !evdref pred in
@@ -674,7 +675,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		 { utj_val = v;
 		   utj_type = s }
 	   | None ->
-	       let s = new_Type_sort () in
+	       let s = evd_comb0 new_sort_variable evdref in
 		 { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
 		   utj_type = s})
     | c ->
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 9888821d14..cd848984d4 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -146,11 +146,12 @@ let print_env env =
 
 let set_module m = current_module := m*)
 
-let new_univ =
+let new_univ_level =
   let univ_gen = ref 0 in
   (fun sp ->
     incr univ_gen;
-    Univ.make_univ (Lib.library_dp(),!univ_gen))
+    Univ.make_universe_level (Lib.library_dp(),!univ_gen))
+let new_univ () = Univ.make_universe (new_univ_level ())
 let new_Type () = mkType (new_univ ())
 let new_Type_sort () = Type (new_univ ())
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 1350743d5d..71e781aeb8 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -14,6 +14,7 @@ open Sign
 open Environ
 
 (** Universes *)
+val new_univ_level : unit -> Univ.universe_level
 val new_univ : unit -> Univ.universe
 val new_sort_in_family : sorts_family -> sorts
 val new_Type : unit -> types