Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Universes.

Needed to exponse compare_head_gen(_leq) so that it could be reused in Universes.
Remove unused functions from univ as well and refactor a little bit.
Changed the syntax to Type@{} for explicit universe level specs, following the WG decision.

7 files changed, 93 insertions, 331 deletions

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 532d44d9e..9be04c765 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -578,9 +578,9 @@ let leq_constr_univs univs m n =
       compare_leq m n
 
 let eq_constr_univs_infer univs m n =
-  if m == n then true, UniverseConstraints.empty
+  if m == n then true, Constraint.empty
   else 
-    let cstrs = ref UniverseConstraints.empty in
+    let cstrs = ref Constraint.empty in
     let eq_universes strict = Univ.Instance.check_eq univs in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
@@ -588,7 +588,7 @@ let eq_constr_univs_infer univs m n =
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
 	  if Univ.check_eq univs u1 u2 then true
 	  else
-	    (cstrs := Univ.UniverseConstraints.add (u1, Univ.UEq, u2) !cstrs;
+	    (cstrs := Univ.enforce_eq u1 u2 !cstrs;
 	     true)
     in
     let rec eq_constr' m n = 
@@ -598,16 +598,16 @@ let eq_constr_univs_infer univs m n =
       res, !cstrs
 
 let leq_constr_univs_infer univs m n =
-  if m == n then true, UniverseConstraints.empty
+  if m == n then true, Constraint.empty
   else 
-    let cstrs = ref UniverseConstraints.empty in
+    let cstrs = ref Constraint.empty in
     let eq_universes strict l l' = Univ.Instance.check_eq univs l l' in
     let eq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
 	  if Univ.check_eq univs u1 u2 then true
-	  else (cstrs := Univ.UniverseConstraints.add (u1, Univ.UEq, u2) !cstrs;
+	  else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
 		true)
     in
     let leq_sorts s1 s2 = 
@@ -616,7 +616,7 @@ let leq_constr_univs_infer univs m n =
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
 	  if Univ.check_leq univs u1 u2 then true
 	  else
-	    (cstrs := Univ.UniverseConstraints.add (u1, Univ.ULe, u2) !cstrs; 
+	    (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
 	     true)
     in
     let rec eq_constr' m n = 
@@ -628,53 +628,6 @@ let leq_constr_univs_infer univs m n =
     let res = compare_leq m n in
       res, !cstrs
 
-let eq_constr_universes m n =
-  if m == n then true, UniverseConstraints.empty
-  else 
-    let cstrs = ref UniverseConstraints.empty in
-    let eq_universes strict l l' = 
-      cstrs := Univ.enforce_eq_instances_univs strict l l' !cstrs; true in
-    let eq_sorts s1 s2 = 
-      if Sorts.equal s1 s2 then true
-      else
-	(cstrs := Univ.UniverseConstraints.add 
-	   (Sorts.univ_of_sort s1, Univ.UEq, Sorts.univ_of_sort s2) !cstrs;
-	 true)
-    in
-    let rec eq_constr' m n = 
-      m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
-    in
-    let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in
-      res, !cstrs
-
-let leq_constr_universes m n =
-  if m == n then true, UniverseConstraints.empty
-  else 
-    let cstrs = ref UniverseConstraints.empty in
-    let eq_universes strict l l' = 
-      cstrs := Univ.enforce_eq_instances_univs strict l l' !cstrs; true in
-    let eq_sorts s1 s2 = 
-      if Sorts.equal s1 s2 then true
-      else (cstrs := Univ.UniverseConstraints.add 
-	      (Sorts.univ_of_sort s1,Univ.UEq,Sorts.univ_of_sort s2) !cstrs; 
-	    true)
-    in
-    let leq_sorts s1 s2 = 
-      if Sorts.equal s1 s2 then true
-      else 
-	(cstrs := Univ.UniverseConstraints.add 
-	   (Sorts.univ_of_sort s1,Univ.ULe,Sorts.univ_of_sort s2) !cstrs; 
-	 true)
-    in
-    let rec eq_constr' m n = 
-      m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
-    in
-    let rec compare_leq m n =
-      compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
-    and leq_constr' m n = m == n || compare_leq m n in
-    let res = compare_leq m n in
-      res, !cstrs
-
 let always_true _ _ = true
 
 let rec eq_constr_nounivs m n =
diff --git a/kernel/constr.mli b/kernel/constr.mli
index c57c4c59b..58f248b03 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -212,19 +212,11 @@ val leq_constr_univs : constr Univ.check_function
 
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [u]. *)
-val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.universe_constrained
+val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained
 
 (** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
     alpha, casts, application grouping and the universe inequalities in [u]. *)
-val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.universe_constrained
-
-(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
-   application grouping and the universe equalities in [c]. *)
-val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained
-
-(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
-    alpha, casts, application grouping and the universe inequalities in [c]. *)
-val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained
+val leq_constr_univs_infer : Univ.universes -> constr -> constr -> bool Univ.constrained
 
 (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping and ignoring universe instances. *)
@@ -281,6 +273,31 @@ val iter_with_binders :
 
 val compare_head : (constr -> constr -> bool) -> constr -> constr -> bool
 
+(** [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
+   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
+   instances (the first boolean tells if they belong to a constant), [s] to 
+   compare sorts; Cast's, binders name and Cases annotations are not taken 
+    into account *)
+
+val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  (Sorts.t -> Sorts.t -> bool) ->
+  (constr -> constr -> bool) ->
+  constr -> constr -> bool
+
+(** [compare_head_gen_leq u s sle f fle c1 c2] compare [c1] and [c2]
+    using [f] to compare the immediate subterms of [c1] of [c2] for
+    conversion, [fle] for cumulativity, [u] to compare universe
+    instances (the first boolean tells if they belong to a constant),
+    [s] to compare sorts for equality and [sle] for subtyping; Cast's,
+    binders name and Cases annotations are not taken into account *)
+
+val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  (Sorts.t -> Sorts.t -> bool) ->
+  (Sorts.t -> Sorts.t -> bool) ->
+  (constr -> constr -> bool) ->
+  (constr -> constr -> bool) ->
+  constr -> constr -> bool
+  
 (** {6 Hashconsing} *)
 
 val hash : constr -> int
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 6a8f3ddd7..a6e107d3f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -664,7 +664,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
     if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2
     else Constr.eq_constr_univs_infer univs t1 t2
   in
-    if b then (Univ.to_constraints univs cstrs)
+    if b then cstrs
     else
       let univs = ((univs, Univ.Constraint.empty), infered_universes) in
       let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in
diff --git a/kernel/term.ml b/kernel/term.ml
index b85c525d1..3b6b69a28 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -140,8 +140,6 @@ let mkCoFix = Constr.mkCoFix
 let eq_constr = Constr.equal
 let eq_constr_univs = Constr.eq_constr_univs
 let leq_constr_univs = Constr.leq_constr_univs
-let eq_constr_universes = Constr.eq_constr_universes
-let leq_constr_universes = Constr.leq_constr_universes
 let eq_constr_nounivs = Constr.eq_constr_nounivs
 
 let kind_of_term = Constr.kind
diff --git a/kernel/term.mli b/kernel/term.mli
index 2d3df6e1e..5ff5f9ba1 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -421,22 +421,14 @@ val mkCoFix : cofixpoint -> constr
 val eq_constr : constr -> constr -> bool
 (** Alias for [Constr.equal] *)
 
-(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
-   application grouping and the universe equalities in [c]. *)
+(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
+   application grouping and the universe constraints in [u]. *)
 val eq_constr_univs : constr Univ.check_function
 
-(** [leq_constr_univs a b] [true, c] if [a] is convertible to [b] modulo 
-    alpha, casts, application grouping and the universe inequalities in [c]. *)
+(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo 
+    alpha, casts, application grouping and the universe constraints in [u]. *)
 val leq_constr_univs : constr Univ.check_function
 
-(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts,
-   application grouping and the universe equalities in [c]. *)
-val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained
-
-(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo
-    alpha, casts, application grouping and the universe inequalities in [c]. *)
-val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained
-
 (** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts,
    application grouping and ignoring universe instances. *)
 val eq_constr_nounivs : constr -> constr -> bool
diff --git a/kernel/univ.ml b/kernel/univ.ml
index bb034c56f..18064d246 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -712,13 +712,20 @@ end
 
 type universe = Universe.t
 
-open Universe
+(* The level of predicative Set *)
+let type0m_univ = Universe.type0m
+let type0_univ = Universe.type0
+let type1_univ = Universe.type1
+let is_type0m_univ = Universe.is_type0m
+let is_type0_univ = Universe.is_type0
+let is_univ_variable l = Universe.level l != None
+let is_small_univ = Universe.is_small
+let pr_uni = Universe.pr
 
-(* type universe_list = UList.t *)
-(* let pr_universe_list = UList.pr *)
+let sup = Universe.sup
+let super = Universe.super
 
-let pr_uni = Universe.pr
-let is_small_univ = Universe.is_small
+open Universe
 
 let universe_level = Universe.level
 
@@ -760,20 +767,6 @@ let enter_equiv_arc u v g =
 let enter_arc ca g =
   UMap.add ca.univ (Canonical ca) g
 
-let is_type0m_univ = Universe.is_type0m
-
-(* The level of predicative Set *)
-let type0m_univ = Universe.type0m
-let type0_univ = Universe.type0
-let type1_univ = Universe.type1
-
-let sup = Universe.sup
-let super = Universe.super
-
-let is_type0_univ = Universe.is_type0
-
-let is_univ_variable l = Universe.level l != None
-
 (* Every Level.t has a unique canonical arc representative *)
 
 (* repr : universes -> Level.t -> canonical_arc *)
@@ -1075,12 +1068,6 @@ let check_eq_univs g l1 l2 =
 let check_eq g u v =
   Universe.equal u v || check_eq_univs g u v
 
-let check_eq = 
-  if Flags.profile then
-    let check_eq_key = Profile.declare_profile "check_eq" in
-      Profile.profile3 check_eq_key check_eq
-  else check_eq
-
 let check_smaller_expr g (u,n) (v,m) =
   let diff = n - m in
     match diff with
@@ -1101,12 +1088,6 @@ let check_leq g u v =
     Universe.is_type0m u ||
     check_eq_univs g u v || real_check_leq g u v
 
-let check_leq = 
-  if Flags.profile then 
-    let check_leq_key = Profile.declare_profile "check_leq" in
-      Profile.profile3 check_leq_key check_leq
-  else check_leq
-
 (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
 
 (** To speed up tests of Set </<= i *)
@@ -1297,7 +1278,6 @@ let pr_constraint_type op =
     | Eq -> " = "
   in str op_str
 
-
 module UConstraintOrd =
 struct
   type t = univ_constraint
@@ -1356,60 +1336,6 @@ module Hconstraints =
 let hcons_constraint = Hashcons.simple_hcons Hconstraint.generate Level.hcons
 let hcons_constraints = Hashcons.simple_hcons Hconstraints.generate hcons_constraint
 
-type universe_constraint_type = ULe | UEq | ULub
-
-type universe_constraint = universe * universe_constraint_type * universe
-module UniverseConstraints = struct
-  module S = Set.Make(
-  struct 
-    type t = universe_constraint
-
-    let compare_type c c' =
-      match c, c' with
-      | ULe, ULe -> 0
-      | ULe, _ -> -1
-      | _, ULe -> 1
-      | UEq, UEq -> 0
-      | UEq, _ -> -1
-      | ULub, ULub -> 0
-      | ULub, _ -> 1
-      
-    let compare (u,c,v) (u',c',v') =
-      let i = compare_type c c' in
-	if Int.equal i 0 then
-	  let i' = Universe.compare u u' in
-	    if Int.equal i' 0 then Universe.compare v v'
-	    else 
-	      if c != ULe && Universe.compare u v' = 0 && Universe.compare v u' = 0 then 0
-	      else i'
-	else i
-  end)
-  
-  include S
-  
-  let add (l,d,r as cst) s = 
-    if Universe.equal l r then s
-    else add cst s
-
-  let tr_dir = function
-    | ULe -> Le
-    | UEq -> Eq
-    | ULub -> Eq
-
-  let op_str = function ULe -> " <= " | UEq -> " = " | ULub -> " /\\ "
-
-  let pr c =
-    fold (fun (u1,op,u2) pp_std ->
-	pp_std ++ Universe.pr u1 ++ str (op_str op) ++
-	Universe.pr u2 ++ fnl ()) c (str "")
-
-  let equal x y = 
-    x == y || equal x y
-
-end
-
-type universe_constraints = UniverseConstraints.t
-type 'a universe_constrained = 'a * universe_constraints
 
 (** A value with universe constraints. *)
 type 'a constrained = 'a * constraints
@@ -1506,22 +1432,6 @@ struct
   let hash = HInstancestruct.hash
     
   let share a = (a, hash a)
-
-    (* let len = Array.length a in *)
-    (*   if Int.equal len 0 then (empty, 0) *)
-    (*   else begin *)
-    (* 	let accu = ref 0 in *)
-    (* 	  for i = 0 to len - 1 do *)
-    (* 	    let l = Array.unsafe_get a i in *)
-    (* 	    let l', h = Level.hcons l, Level.hash l in *)
-    (* 	      accu := Hashset.Combine.combine !accu h; *)
-    (* 	      if l' == l then ()  *)
-    (* 	      else Array.unsafe_set a i l' *)
-    (* 	  done; *)
-    (* 	  (\* [h] must be positive. *\) *)
-    (* 	  let h = !accu land 0x3FFFFFFF in *)
-    (* 	    (a, h) *)
-    (*   end *)
 	      
   let empty = hcons [||]
 
@@ -1563,11 +1473,6 @@ struct
 	 (* Necessary as universe instances might come from different modules and 
 	    unmarshalling doesn't preserve sharing *))
 
-	 (* if b then *)
-	 (*   (prerr_endline ("Not physically equal but equal:" ^(Pp.string_of_ppcmds (pr t)) *)
-	 (* 		   ^ " and " ^ (Pp.string_of_ppcmds (pr u))); b) *)
-	 (* else b) *)
-
   let check_eq g t1 t2 =
     t1 == t2 ||
       (Int.equal (Array.length t1) (Array.length t2) &&
@@ -1677,29 +1582,6 @@ let pr_universe_level_subst =
 
 let constraints_of (_, cst) = cst
 
-let remove_dangling_constraints dangling cst =
-  Constraint.fold (fun (l,d,r as cstr) cst' -> 
-    if List.mem l dangling || List.mem r dangling then cst'
-    else
-      (** Unnecessary constraints Prop <= u *)
-      if Level.equal l Level.prop && d == Le then cst'
-      else Constraint.add cstr cst') cst Constraint.empty
-  
-let check_context_subset (univs, cst) (univs', cst') =
-  let newunivs, dangling = List.partition (fun u -> LSet.mem u univs) (Instance.to_list univs') in
-    (* Some universe variables that don't appear in the term 
-       are still mentionned in the constraints. This is the 
-       case for "fake" universe variables that correspond to +1s. *)
-    (* if not (CList.is_empty dangling) then  *)
-    (*   todo ("A non-empty set of inferred universes do not appear in the term or type"); *)
-      (* (not (constraints_depend cst' dangling));*)
-    (* TODO: check implication *)
-  (** Remove local universes that do not appear in any constraint, they
-      are really entirely parametric. *)
-  (* let newunivs, dangling' = List.partition (fun u -> constraints_depend cst [u]) newunivs in *)
-  let cst' = remove_dangling_constraints dangling cst in
-    Instance.of_list newunivs, cst'
-
 (** Substitutions. *)
 
 let make_universe_subst inst (ctx, csts) = 
@@ -1721,12 +1603,6 @@ let subst_univs_level_level subst l =
   try LMap.find l subst
   with Not_found -> l
 
-let rec normalize_univs_level_level subst l =
-  try 
-    let l' = LMap.find l subst in
-      normalize_univs_level_level subst l'
-  with Not_found -> l
-
 let subst_univs_level_universe subst u =
   let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in
   let u' = Universe.smartmap f u in
@@ -1744,10 +1620,6 @@ let subst_univs_level_constraints subst csts =
     (fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
     csts Constraint.empty 
 
-(* let subst_univs_level_constraint_key = Profile.declare_profile "subst_univs_level_constraint";; *)
-(* let subst_univs_level_constraint = *)
-(*   Profile.profile2 subst_univs_level_constraint_key subst_univs_level_constraint *)
-
 (** With level to universe substitutions. *)
 type universe_subst_fn = universe_level -> universe
 
@@ -1782,11 +1654,6 @@ let subst_univs_constraint fn (u,d,v) =
     if d != Lt && Universe.equal u' v' then None
     else Some (u',d,v')
 
-let subst_univs_universe_constraint fn (u,d,v) =
-  let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in
-    if Universe.equal u' v' then None
-    else Some (u',d,v')
-
 (** Constraint functions. *)
 
 type 'a constraint_function = 'a -> 'a -> constraints -> constraints
@@ -1850,29 +1717,13 @@ let enforce_leq_level u v c =
 let enforce_eq_instances x y = 
   let ax = Instance.to_array x and ay = Instance.to_array y in
     if Array.length ax != Array.length ay then
-      anomaly (Pp.str "Invalid argument: enforce_eq_instances called with instances of different lengths");
+      anomaly (Pp.(++) (Pp.str "Invalid argument: enforce_eq_instances called with")
+		 (Pp.str " instances of different lengths"));
     CArray.fold_right2 enforce_eq_level ax ay
-
-type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
-
-let enforce_eq_instances_univs strict x y c = 
-  let d = if strict then ULub else UEq in
-  let ax = Instance.to_array x and ay = Instance.to_array y in
-    if Array.length ax != Array.length ay then
-      anomaly (Pp.str "Invalid argument: enforce_eq_instances_univs called with instances of different lengths");    
-    CArray.fold_right2
-      (fun x y -> UniverseConstraints.add (Universe.make x, d, Universe.make y))
-      ax ay c
       
 let merge_constraints c g =
   Constraint.fold enforce_constraint c g
 
-let merge_constraints = 
-  if Flags.profile then 
-    let key = Profile.declare_profile "merge_constraints" in
-      Profile.profile2 key merge_constraints
-  else merge_constraints
-
 let check_constraint g (l,d,r) =
   match d with
   | Eq -> check_equal g l r
@@ -1882,12 +1733,6 @@ let check_constraint g (l,d,r) =
 let check_constraints c g =
   Constraint.for_all (check_constraint g) c
 
-let check_constraints =
-  if Flags.profile then
-    let key = Profile.declare_profile "check_constraints" in
-      Profile.profile2 key check_constraints
-  else check_constraints
-
 let enforce_univ_constraint (u,d,v) =
   match d with
   | Eq -> enforce_eq u v
@@ -1899,41 +1744,10 @@ let subst_univs_constraints subst csts =
     (fun c -> Option.fold_right enforce_univ_constraint (subst_univs_constraint subst c))
     csts Constraint.empty 
 
-(* let subst_univs_constraints_key = Profile.declare_profile "subst_univs_constraints";; *)
-(* let subst_univs_constraints = *)
-(*   Profile.profile2 subst_univs_constraints_key subst_univs_constraints *)
-
-let subst_univs_universe_constraints subst csts =
-  UniverseConstraints.fold 
-    (fun c -> Option.fold_right UniverseConstraints.add (subst_univs_universe_constraint subst c))
-    csts UniverseConstraints.empty 
-
-(* let subst_univs_universe_constraints_key = Profile.declare_profile "subst_univs_universe_constraints";; *)
-(* let subst_univs_universe_constraints = *)
-(*   Profile.profile2 subst_univs_universe_constraints_key subst_univs_universe_constraints *)
-
 (** Substitute instance inst for ctx in csts *)
 let instantiate_univ_context subst (_, csts) = 
   subst_univs_level_constraints subst csts
 
-let check_consistent_constraints (ctx,cstrs) cstrs' =
-  (* TODO *) ()
-
-let to_constraints g s = 
-  let tr (x,d,y) acc =
-    let add l d l' acc = Constraint.add (l,UniverseConstraints.tr_dir d,l') acc in
-      match Universe.level x, d, Universe.level y with
-      | Some l, (ULe | UEq | ULub), Some l' -> add l d l' acc
-      | _, ULe, Some l' -> enforce_leq x y acc
-      | _, ULub, _ -> acc
-      | _, d, _ -> 
-	let f = if d == ULe then check_leq else check_eq in
-	  if f g x y then acc else 
-	    raise (Invalid_argument 
-		   "to_constraints: non-trivial algebraic constraint between universes")
-  in UniverseConstraints.fold tr s Constraint.empty
-     
-
 (* Normalization *)
 
 let lookup_level u g =
@@ -2288,3 +2102,30 @@ let explain_universe_inconsistency (o,u,v,p) =
 let compare_levels = Level.compare
 let eq_levels = Level.equal
 let equal_universes = Universe.equal
+
+
+(*
+
+let merge_constraints = 
+  if Flags.profile then 
+    let key = Profile.declare_profile "merge_constraints" in
+      Profile.profile2 key merge_constraints
+  else merge_constraints
+let check_constraints =
+  if Flags.profile then
+    let key = Profile.declare_profile "check_constraints" in
+      Profile.profile2 key check_constraints
+  else check_constraints
+
+let check_eq = 
+  if Flags.profile then
+    let check_eq_key = Profile.declare_profile "check_eq" in
+      Profile.profile3 check_eq_key check_eq
+  else check_eq
+
+let check_leq = 
+  if Flags.profile then 
+    let check_leq_key = Profile.declare_profile "check_leq" in
+      Profile.profile3 check_leq_key check_leq
+  else check_leq
+*)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 74bd01610..3fc2c7dc2 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -182,6 +182,9 @@ val initial_universes : universes
 
 val is_initial_universes : universes -> bool
 
+val sort_universes : universes -> universes
+
+(** Adds a universe to the graph, ensuring it is >= Prop. *)
 val add_universe : universe_level -> universes -> universes
 
 (** {6 Substitution} *)
@@ -267,6 +270,8 @@ val eq_constraint : constraints -> constraints -> bool
 (** A value with universe constraints. *)
 type 'a constrained = 'a * constraints
 
+(** Constrained *)
+val constraints_of : 'a constrained -> constraints
 
 (** A list of universes with universe constraints,
     representiong local universe variables and constraints *)
@@ -307,8 +312,7 @@ sig
   val add_constraints : t -> constraints -> t
   val add_universes : Instance.t -> t -> t
 
-  (** Arbitrary choice of linear order of the variables 
-      and normalization of the constraints *)
+  (** Arbitrary choice of linear order of the variables *)
   val to_context : t -> universe_context
   val of_context : universe_context -> t
 
@@ -326,77 +330,39 @@ type universe_context_set = ContextSet.t
 type 'a in_universe_context = 'a * universe_context
 type 'a in_universe_context_set = 'a * universe_context_set
 
-(** {6 Constraints for type inference}
-    
-    When doing conversion of universes, not only do we have =/<= constraints but
-    also Lub constraints which correspond to unification of two levels that might
-    not be necessary if unfolding is performed.
- *)
-
-type universe_constraint_type = ULe | UEq | ULub
-
-type universe_constraint = universe * universe_constraint_type * universe
-module UniverseConstraints : sig
-  include Set.S with type elt = universe_constraint
-			     
-  val pr : t -> Pp.std_ppcmds
-end
-
-type universe_constraints = UniverseConstraints.t
-type 'a universe_constrained = 'a * universe_constraints
-
-
-(** Constrained *)
-val constraints_of : 'a constrained -> constraints
-
-
-(** [check_context_subset s s'] checks that [s] is implied by [s'] as a set of constraints,
-    and shrinks [s'] to the set of variables declared in [s].
-. *)
-val check_context_subset : universe_context_set -> universe_context -> universe_context
-
-(** Make a universe level substitution: the list must match the context variables. *)
-val make_universe_subst : Instance.t -> universe_context -> universe_level_subst
-
 val empty_level_subst : universe_level_subst
 val is_empty_level_subst : universe_level_subst -> bool
 
-(** Get the instantiated graph. *)
-val instantiate_univ_context : universe_level_subst -> universe_context -> constraints
-
 (** Substitution of universes. *)
 val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
 val subst_univs_level_universe : universe_level_subst -> universe -> universe
 val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
 
-val normalize_univs_level_level : universe_level_subst -> universe_level -> universe_level
+(** Make a universe level substitution: the instances must match. *)
+val make_universe_subst : Instance.t -> universe_context -> universe_level_subst
+(** Get the instantiated graph. *)
+val instantiate_univ_context : universe_level_subst -> universe_context -> constraints
 
+(** Level to universe substitutions. *)
 
 val empty_subst : universe_subst
 val is_empty_subst : universe_subst -> bool
 val make_subst : universe_subst -> universe_subst_fn
 
-(* val subst_univs_level_fail : universe_subst_fn -> universe_level -> universe_level *)
 val subst_univs_level : universe_subst_fn -> universe_level -> universe
 val subst_univs_universe : universe_subst_fn -> universe -> universe
 val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
-val subst_univs_universe_constraints : universe_subst_fn -> universe_constraints -> universe_constraints
 
-(** Raises universe inconsistency if not compatible. *)
-val check_consistent_constraints : universe_context_set -> constraints -> unit
+(** Enforcing constraints. *)
 
 type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
-val enforce_leq : universe constraint_function
 val enforce_eq : universe constraint_function
+val enforce_leq : universe constraint_function
 val enforce_eq_level : universe_level constraint_function
 val enforce_leq_level : universe_level constraint_function
 val enforce_eq_instances : universe_instance constraint_function
 
-type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
-
-val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_function
-
 (** {6 ... } *)
 (** Merge of constraints in a universes graph.
   The function [merge_constraints] merges a set of constraints in a given
@@ -422,16 +388,12 @@ exception UniverseInconsistency of univ_inconsistency
 
 val enforce_constraint : univ_constraint -> universes -> universes
 val merge_constraints : constraints -> universes -> universes
-val sort_universes : universes -> universes
 
 val constraints_of_universes : universes -> constraints
 
-val to_constraints : universes -> universe_constraints -> constraints
-
 val check_constraint  : universes -> univ_constraint -> bool
 val check_constraints : constraints -> universes -> bool
 
-
 (** {6 Support for sort-polymorphism } *)
 
 val solve_constraints_system : universe option array -> universe array -> universe array ->
@@ -455,7 +417,6 @@ val univ_depends : universe -> universe -> bool
 val pr_universes : universes -> Pp.std_ppcmds
 val pr_constraint_type : constraint_type -> Pp.std_ppcmds
 val pr_constraints : constraints -> Pp.std_ppcmds
-(* val pr_universe_list : universe_list -> Pp.std_ppcmds *)
 val pr_universe_context : universe_context -> Pp.std_ppcmds
 val pr_universe_context_set : universe_context_set -> Pp.std_ppcmds
 val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds