- Rename eq to equal in Univ, document new modules, set interfaces.

  A try at hashconsing all universes instances seems to incur a big cost.
- Do hashconsing of universe instances in constr.
- Little fix in obligations w.r.t. non-polymorphic constants.

Conflicts:
	kernel/constr.ml
	kernel/declareops.ml
	kernel/inductive.ml
	kernel/univ.mli

17 files changed, 345 insertions, 198 deletions

diff --git a/checker/term.ml b/checker/term.ml
index 67d380336..ea81f5dab 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -347,7 +347,7 @@ let compare_sorts s1 s2 = match s1, s2 with
   | Pos, Null -> false
   | Null, Pos -> false
   end
-| Type u1, Type u2 -> Universe.eq u1 u2
+| Type u1, Type u2 -> Universe.equal u1 u2
 | Prop _, Type _ -> false
 | Type _, Prop _ -> false
 
diff --git a/kernel/closure.ml b/kernel/closure.ml
index fd3ab525e..a1a9b54f7 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -209,7 +209,7 @@ let unfold_red kn =
 type table_key = constant puniverses tableKey
 
 let eq_pconstant_key (c,u) (c',u') =
-  eq_constant_key c c' && Univ.Instance.eq u u'
+  eq_constant_key c c' && Univ.Instance.equal u u'
   
 module IdKeyHash =
 struct
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 89c138a08..ac2c4418e 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -496,7 +496,7 @@ let compare_head_gen eq_universes eq_sorts f t1 t2 =
       Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
   | _ -> false
 
-let compare_head = compare_head_gen (fun _ -> Univ.Instance.eq) Sorts.equal
+let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
 
 (* [compare_head_gen_leq u s sl eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
    the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
@@ -541,10 +541,10 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
 (* alpha conversion : ignore print names and casts *)
 
 let rec eq_constr m n =
-  (m == n) || compare_head_gen (fun _ -> Univ.Instance.eq) Sorts.equal eq_constr m n
+  (m == n) || compare_head_gen (fun _ -> Instance.equal) Sorts.equal eq_constr m n
 
 (** Strict equality of universe instances. *)
-let compare_constr = compare_head_gen (fun _ -> Univ.Instance.eq) Sorts.equal
+let compare_constr = compare_head_gen (fun _ -> Instance.equal) Sorts.equal
 
 let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
@@ -726,7 +726,7 @@ let hasheq t1 t2 =
     | Proj (c1,t1), Proj (c2,t2) -> c1 == c2 && t1 == t2
     | App (c1,l1), App (c2,l2) -> c1 == c2 && array_eqeq l1 l2
     | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && array_eqeq l1 l2
-    | Const (c1,u1), Const (c2,u2) -> c1 == c2 && Univ.Instance.eqeq u1 u2
+    | Const (c1,u1), Const (c2,u2) -> c1 == c2 && u1 == u2
     | Ind ((sp1,i1),u1), Ind ((sp2,i2),u2) -> 
       sp1 == sp2 && Int.equal i1 i2 && Univ.Instance.eqeq u1 u2
     | Construct (((sp1,i1),j1),u1), Construct (((sp2,i2),j2),u2) ->
@@ -769,7 +769,7 @@ let hash_cast_kind = function
 | DEFAULTcast -> 2
 | REVERTcast -> 3
 
-let hash_instance = Univ.Instance.hcons
+let sh_instance = Univ.Instance.share
 
 (* [hashcons hash_consing_functions constr] computes an hash-consed
    representation for [constr] using [hash_consing_functions] on
@@ -808,13 +808,19 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) =
       | Proj (p,c) ->
         let c, hc = sh_rec c in
         let p' = sh_con p in
-          (Proj (p', c), combinesmall 17 (Hashtbl.hash p')) (** FIXME *)
+          (Proj (p', c), combinesmall 17 (Hashtbl.hash p'))
       | Const (c,u) ->
-	(Const (sh_con c, hash_instance u), combinesmall 9 (Constant.hash c))
-      | Ind (ind, u) ->
-	(Ind (sh_ind ind, hash_instance u), combinesmall 10 (ind_hash ind))
-      | Construct (c, u) ->
-	(Construct (sh_construct c, hash_instance u), combinesmall 11 (constructor_hash c))
+	let c' = sh_con c in
+	let u', hu = sh_instance u in
+	(Const (c', u'), combinesmall 9 (combine (Constant.hash c) hu))
+      | Ind ((kn,i) as ind,u) ->
+	let u', hu = sh_instance u in
+	(Ind (sh_ind ind, u'), 
+	 combinesmall 10 (combine (ind_hash ind) hu))
+      | Construct ((((kn,i),j) as c,u))->
+	let u', hu = sh_instance u in
+	(Construct (sh_construct c, u'),
+	 combinesmall 11 (combine (constructor_hash c) hu))
       | Case (ci,p,c,bl) ->
 	let p, hp = sh_rec p
 	and c, hc = sh_rec c in
@@ -887,15 +893,15 @@ let rec hash t =
     | App (c,l) ->
       combinesmall 7 (combine (hash_term_array l) (hash c))
     | Proj (p,c) ->
-      combinesmall 17 (combine (Hashtbl.hash p) (hash c))
+      combinesmall 17 (combine (Constant.hash p) (hash c))
     | Evar (e,l) ->
       combinesmall 8 (combine (Evar.hash e) (hash_term_array l))
-    | Const (c, _) ->
-      combinesmall 9 (Constant.hash c)
-    | Ind (ind, _) ->
-      combinesmall 10 (ind_hash ind)
-    | Construct (c, _) ->
-      combinesmall 11 (constructor_hash c)
+    | Const (c,u) ->
+      combinesmall 9 (combine (Constant.hash c) (Instance.hash u))
+    | Ind (ind,u) ->
+      combinesmall 10 (combine (ind_hash ind) (Instance.hash u))
+    | Construct (c,u) ->
+      combinesmall 11 (combine (constructor_hash c) (Instance.hash u))
     | Case (_ , p, c, bl) ->
       combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl))
     | Fix (ln ,(_, tl, bl)) ->
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index be6c18810..92a566b7c 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -195,6 +195,7 @@ let subst_regular_ind_arity sub s =
 
 let subst_template_ind_arity sub s = s
 
+(* FIXME records *)
 let subst_ind_arity =
   subst_decl_arity subst_regular_ind_arity subst_template_ind_arity
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index ef0f0ca4d..ede655702 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -232,10 +232,6 @@ let constant_type env (kn,u) =
 	(map_regular_arity (subst_univs_constr subst) cb.const_type, csts)
     else cb.const_type, Univ.Constraint.empty
 
-let constant_type_in_ctx env kn =
-  let cb = lookup_constant kn env in
-    cb.const_type, Future.force cb.const_universes
-
 let constant_context env kn =
   let cb = lookup_constant kn env in
     if cb.const_polymorphic then Future.force cb.const_universes
diff --git a/kernel/environ.mli b/kernel/environ.mli
index d885ddd56..28eecc7ef 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -144,7 +144,6 @@ exception NotEvaluableConst of const_evaluation_result
 
 val constant_value : env -> constant puniverses -> constr constrained
 val constant_type : env -> constant puniverses -> constant_type constrained
-val constant_type_in_ctx : env -> constant -> constant_type Univ.in_universe_context
 
 val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option
 val constant_value_and_type : env -> constant puniverses -> 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 64a6f1e17..7cf5dd62d 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -156,8 +156,8 @@ let sort_as_univ = function
 
 let cons_subst u su subst =
   try
-    (u, Universe.sup su (List.assoc_f Universe.eq u subst)) ::
-      List.remove_assoc_f Universe.eq u subst
+    (u, sup su (List.assoc_f Universe.equal u subst)) ::
+      List.remove_assoc_f Universe.equal u subst
   with Not_found -> (u, su) :: subst
 
 let actualize_decl_level env lev t =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8322a7e96..5d565b89e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -49,7 +49,10 @@ module Level = struct
       let hashcons hdir = function
 	| Prop as x -> x
 	| Set as x -> x
-	| Level (n,d) -> Level (n,hdir d)
+	| Level (n,d) as x -> 
+	  let d' = hdir d in
+	    if d' == d then x else Level (n,d')
+			   
       let equal l1 l2 =
         l1 == l2 ||
         match l1,l2 with
@@ -62,6 +65,7 @@ module Level = struct
     end)
   
   let hcons = Hashcons.simple_hcons Hunivlevel.generate Names.DirPath.hcons
+  let hash = Hashtbl.hash
 
   let make m n = hcons (Level (n, m))
 
@@ -109,7 +113,7 @@ module Level = struct
       Int.equal i1 i2 && DirPath.equal dp1 dp2
     | _ -> false
 
-  let eq u v = u == v
+  let equal u v = u == v
   let leq u v = compare u v <= 0
 
   let to_string = function
@@ -206,8 +210,8 @@ module LList = struct
     Hashcons.simple_hcons Huniverse_level_list.generate Level.hcons
 
   let empty = hcons []
-  let eq l l' = l == l' ||
-    (try List.for_all2 Level.eq l l'
+  let equal l l' = l == l' ||
+    (try List.for_all2 Level.equal l l'
      with Invalid_argument _ -> false)
 
   let levels =
@@ -222,9 +226,6 @@ type universe_level_subst_fn = universe_level -> universe_level
 type universe_set = LSet.t
 type 'a universe_map = 'a LMap.t
 
-let compare_levels = Level.compare
-let eq_levels = Level.eq
-
 module Hashconsing = struct
   module Uid = struct
     type t = int
@@ -572,9 +573,9 @@ struct
       | (l, 0) -> Level.is_small l
       | _ -> false
 
-    (* let eq (u,n) (v,n') = *)
-    (*   Int.equal n n' && Level.eq u v *)
-    let eq x y = x == y
+    (* let equal (u,n) (v,n') = *)
+    (*   Int.equal n n' && Level.equal u v *)
+    let equal x y = x == y
 
     let leq (u,n) (v,n') =
       let cmp = Level.compare u v in
@@ -645,16 +646,14 @@ struct
   type t = Huniv.t
   open Huniv
     
-  let eq x y = x == y (* Huniv.equal *)
+  let equal x y = x == y (* Huniv.equal *)
 
   let compare u1 u2 =
-    if eq u1 u2 then 0 else 
+    if equal u1 u2 then 0 else 
       Huniv.compare compare_expr u1 u2
 
   let hcons_unique = Huniv.make
-  let normalize x = x
-  (* let hcons_unique x = x *)
-  let hcons x = hcons_unique (normalize x)
+  let hcons x = hcons_unique x
 
   let make l = Huniv.tip (Hunivelt.make (Expr.make l))
   let tip x = Huniv.tip (Hunivelt.make x)
@@ -686,7 +685,7 @@ struct
     fold (fun x acc -> LSet.add (Expr.get_level (Hunivelt.node x)) acc) l LSet.empty
 
   let is_small u = 
-    match level (normalize u) with
+    match level u with
     | Some l -> Level.is_small l
     | _ -> false
 
@@ -1365,7 +1364,7 @@ module UniverseConstraints = struct
   include S
   
   let add (l,d,r as cst) s = 
-    if Universe.eq l r then s
+    if Universe.equal l r then s
     else add cst s
 
   let tr_dir = function
@@ -1391,6 +1390,13 @@ type 'a universe_constrained = 'a * universe_constraints
 (** A value with universe constraints. *)
 type 'a constrained = 'a * constraints
 
+(** A universe level substitution, note that no algebraic universes are
+    involved *)
+type universe_level_subst = universe_level universe_map
+
+(** A full substitution might involve algebraic universes *)
+type universe_subst = universe universe_map
+
 let level_subst_of f = 
   fun l -> 
     try let u = f l in 
@@ -1399,66 +1405,145 @@ let level_subst_of f =
 	  | Some l -> l
     with Not_found -> l
      
-module Instance = struct
+module Instance : sig 
+    type t
+
+    val empty : t
+    val is_empty : t -> bool
+      
+    val of_array : Level.t array -> t
+    val to_array : t -> Level.t array
+
+    val of_list : Level.t list -> t
+    val to_list : t -> Level.t list
+
+    val append : t -> t -> t
+    val equal : t -> t -> bool
+    val hcons : t -> t
+    val hash : t -> int
+
+    val share : t -> t * int
+
+    val eqeq : t -> t -> bool
+    val subst_fn : universe_level_subst_fn -> t -> t
+    val subst : universe_level_subst -> t -> t
+    
+    val pr : t -> Pp.std_ppcmds
+    val levels : t -> LSet.t
+    val check_eq : t check_function 
+end = 
+struct
   type t = Level.t array
 
-  module HInstance =
-    Hashcons.Make(
-      struct
-	type _t = t
-	type t = _t
-	type u = Level.t -> Level.t
-	let hashcons huniv a = 
-	  CArray.smartmap huniv a
-
-	let equal t1 t2 =
-	  t1 == t2 ||
-	    (Int.equal (Array.length t1) (Array.length t2) &&
-	       let rec aux i =
-		 (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
-	       in aux 0)
-
-	let hash = Hashtbl.hash
-    end)
+  let empty : t = [||]
 
-  let hcons_instance = Hashcons.simple_hcons HInstance.generate Level.hcons
+  module HInstancestruct =
+  struct
+    type _t = t
+    type t = _t
+    type u = Level.t -> Level.t
+
+    let hashcons huniv a = 
+      let len = Array.length a in
+	if Int.equal len 0 then empty
+	else begin
+	  for i = 0 to len - 1 do
+	    let x = Array.unsafe_get a i in
+	    let x' = huniv x in
+	      if x == x' then ()
+	      else Array.unsafe_set a i x'
+	  done;
+	  a
+	end
+
+    let equal t1 t2 =
+      t1 == t2 ||
+	(Int.equal (Array.length t1) (Array.length t2) &&
+	   let rec aux i =
+	     (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
+	   in aux 0)
+	
+    let hash a = 
+      let accu = ref 0 in
+	for i = 0 to Array.length a - 1 do
+	  let l = Array.unsafe_get a i in
+	  let h = Level.hash l in
+	    accu := Hashset.Combine.combine !accu h;
+	done;
+	(* [h] must be positive. *)
+	let h = !accu land 0x3FFFFFFF in
+	  h
+  end
+
+  module HInstance = Hashcons.Make(HInstancestruct)
+
+  let hcons = Hashcons.simple_hcons HInstance.generate Level.hcons
+    
+  let hash = HInstancestruct.hash
+    
+  let share 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 hcons x = x
+	      
+  let empty = hcons [||]
 
-  let hcons = hcons_instance
-  let empty = [||]
   let is_empty x = Int.equal (Array.length x) 0
 
-  let eq t u = t == u || CArray.for_all2 Level.eq t u
+  let append x y =
+    if Array.length x = 0 then y
+    else if Array.length y = 0 then x 
+    else hcons (Array.append x y)
+
+  let of_array a = hcons a
 
-  let of_array a = a
   let to_array a = a
+
+  let of_list a = of_array (Array.of_list a)
+  let to_list = Array.to_list
+
     
-  let eqeq t1 t2 =
-    t1 == t2 ||
-      (Int.equal (Array.length t1) (Array.length t2) &&
-	 let rec aux i =
-	   (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
-	 in aux 0)
+  let eqeq = HInstancestruct.equal
 
-  let subst_fn fn t = CArray.smartmap fn t
-  let subst s t = CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
+  let subst_fn fn t = 
+    let t' = CArray.smartmap fn t in
+      if t' == t then t else hcons t'
+
+  let subst s t =
+    let t' = 
+      CArray.smartmap (fun x -> try LMap.find x s with Not_found -> x) t
+    in if t' == t then t else hcons t'
 
   let levels x = LSet.of_array x
 
   let pr =
     prvect_with_sep spc Level.pr
 
-  let append x y =
-    if Array.length x = 0 then y
-    else if Array.length y = 0 then x 
-    else Array.append x y
+  let equal t u = 
+    t == u ||
+      (Array.is_empty t && Array.is_empty u) ||
+      (CArray.for_all2 Level.equal t u 
+	 (* Necessary as universe instances might come from different modules and 
+	    unmarshalling doesn't preserve sharing *))
 
-  let max_level i = 
-    if Array.is_empty i then 0
-    else
-      let l = CArray.last i in
-	match l with
-	| Level.Level (i,_) -> i
-	| _ -> assert false
+	 (* 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 ||
@@ -1537,7 +1622,7 @@ struct
     union (of_instance univs) ctx
 
   let to_context (ctx, cst) =
-    (Array.of_list (LSet.elements ctx), cst)
+    (Instance.of_array (Array.of_list (LSet.elements ctx)), cst)
 
   let of_context (ctx, cst) =
     (Instance.levels ctx, cst)
@@ -1557,13 +1642,6 @@ type universe_context_set = ContextSet.t
 type 'a in_universe_context = 'a * universe_context
 type 'a in_universe_context_set = 'a * universe_context_set
 
-(** A universe level substitution, note that no algebraic universes are
-    involved *)
-type universe_level_subst = universe_level universe_map
-
-(** A full substitution might involve algebraic universes *)
-type universe_subst = universe universe_map
-
 (** Pretty-printing *)
 let pr_constraints = Constraint.pr
 
@@ -1580,7 +1658,7 @@ let pr_universe_level_subst =
 let constraints_of (_, cst) = cst
 
 let constraint_depend (l,d,r) u =
-  Level.eq l u || Level.eq l r
+  Level.equal l u || Level.equal l r
 
 let constraint_depend_list (l,d,r) us =
   List.mem l us || List.mem r us
@@ -1593,11 +1671,11 @@ let remove_dangling_constraints dangling cst =
     if List.mem l dangling || List.mem r dangling then cst'
     else
       (** Unnecessary constraints Prop <= u *)
-      if Level.eq l Level.prop && d == Le then cst'
+      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) (Array.to_list univs') in
+  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. *)
@@ -1609,13 +1687,13 @@ let check_context_subset (univs, cst) (univs', cst') =
       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
-    Array.of_list newunivs, cst'
+    Instance.of_list newunivs, cst'
 
 (** Substitutions. *)
 
 let make_universe_subst inst (ctx, csts) = 
   try Array.fold_left2 (fun acc c i -> LMap.add c (Universe.make i) acc)
-        LMap.empty ctx inst
+        LMap.empty (Instance.to_array ctx) (Instance.to_array inst)
   with Invalid_argument _ -> 
     anomaly (Pp.str "Mismatched instance and context when building universe substitution")
 
@@ -1652,7 +1730,7 @@ let rec subst_univs_level_universe subst u =
 let subst_univs_level_constraint subst (u,d,v) =
   let u' = subst_univs_level_level subst u 
   and v' = subst_univs_level_level subst v in
-    if d != Lt && Level.eq u' v' then None
+    if d != Lt && Level.equal u' v' then None
     else Some (u',d,v')
 
 let subst_univs_level_constraints subst csts =
@@ -1695,12 +1773,12 @@ let subst_univs_universe fn ul =
 
 let subst_univs_constraint fn (u,d,v) =
   let u' = subst_univs_level fn u and v' = subst_univs_level fn v in
-    if d != Lt && Universe.eq u' v' then None
+    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.eq u' v' then None
+    if Universe.equal u' v' then None
     else Some (u',d,v')
 
 (** Constraint functions. *)
@@ -1709,7 +1787,7 @@ type 'a constraint_function = 'a -> 'a -> constraints -> constraints
 
 let constraint_add_leq v u c =
   (* We just discard trivial constraints like u<=u *)
-  if Expr.eq v u then c
+  if Expr.equal v u then c
   else 
     match v, u with
     | (x,n), (y,m) -> 
@@ -1717,17 +1795,17 @@ let constraint_add_leq v u c =
       if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
 	Constraint.add (x,Lt,y) c
       else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
-	if Level.eq x y then (* u+(k+1) <= u *)
+	if Level.equal x y then (* u+(k+1) <= u *)
 	  raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, []))
 	else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints")
       else if j = 0 then
 	Constraint.add (x,Le,y) c
       else (* j >= 1 *) (* m = n + k, u <= v+k *)
-	if Level.eq x y then c (* u <= u+k, trivial *)
+	if Level.equal x y then c (* u <= u+k, trivial *)
 	else if Level.is_small x then c (* Prop,Set <= u+S k, trivial *)
 	else anomaly (Pp.str"Unable to handle arbitrary u <= v+k constraints")
 	  
-let check_univ_eq u v = Universe.eq u v
+let check_univ_eq u v = Universe.equal u v
 
 let check_univ_leq_one u v = Universe.exists (Expr.leq u) v
 
@@ -1746,7 +1824,7 @@ let enforce_leq u v c =
 
 let enforce_eq_level u v c =
   (* We discard trivial constraints like u=u *)
-  if Level.eq u v then c 
+  if Level.equal u v then c 
   else if Level.apart u v then
     error_inconsistency Eq u v []
   else Constraint.add (u,Eq,v) c
@@ -1761,16 +1839,17 @@ let enforce_eq u v c =
   else enforce_eq u v c
 
 let enforce_leq_level u v c =
-  if Level.eq u v then c else Constraint.add (u,Le,v) c
+  if Level.equal u v then c else Constraint.add (u,Le,v) c
 
-let enforce_eq_instances = CArray.fold_right2 enforce_eq_level 
+let enforce_eq_instances x y = 
+  CArray.fold_right2 enforce_eq_level (Instance.to_array x) (Instance.to_array y)
 
 type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
 
 let enforce_eq_instances_univs strict t1 t2 c = 
   let d = if strict then ULub else UEq in
     CArray.fold_right2 (fun x y -> UniverseConstraints.add (Universe.make x, d, Universe.make y))
-      t1 t2 c
+      (Instance.to_array t1) (Instance.to_array t2) c
 
 let merge_constraints c g =
   Constraint.fold enforce_constraint c g
@@ -2050,13 +2129,13 @@ let sort_universes orig =
 
 let remove_large_constraint u v min = 
   match Universe.level v with
-  | Some u' -> if Level.eq u u' then min else v
+  | Some u' -> if Level.equal u u' then min else v
   | None -> Huniv.remove (Hunivelt.make (Universe.Expr.make u)) v
 
 (* [is_direct_constraint u v] if level [u] is a member of universe [v] *)
 let is_direct_constraint u v =
   match Universe.level v with
-  | Some u' -> Level.eq u u'
+  | Some u' -> Level.equal u u'
   | None -> Huniv.mem (Hunivelt.make (Universe.Expr.make u)) v
 
 (*
@@ -2189,10 +2268,7 @@ let hcons_universe_set =
 let hcons_universe_context_set (v, c) = 
   (hcons_universe_set v, hcons_constraints c)
 
-
-let hcons_univlevel = Level.hcons
 let hcons_univ x = x (* Universe.hcons (Huniv.node x) *)
-let equal_universes = Universe.equal_universes
 
 let explain_universe_inconsistency (o,u,v,p) =
     let pr_rel = function
@@ -2204,8 +2280,12 @@ let explain_universe_inconsistency (o,u,v,p) =
 	str " because" ++ spc() ++ pr_uni v ++
 	  prlist (fun (r,v) -> spc() ++ pr_rel r ++ str" " ++ pr_uni v)
 	  p ++
-	  (if Universe.eq (snd (List.last p)) u then mt() else
+	  (if Universe.equal (snd (List.last p)) u then mt() else
 	      (spc() ++ str "= " ++ pr_uni u)) 
     in
       str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
         pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")"
+
+let compare_levels = Level.compare
+let eq_levels = Level.equal
+let equal_universes = Universe.equal_universes
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 9e7cc18b4..c149bb1ac 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -16,12 +16,15 @@ sig
 
   val set : t
   val prop : t
+  (** The set and prop universe levels. *)
+
   val is_small : t -> bool
+  (** Is the universe set or prop? *)
 
   val compare : t -> t -> int
   (** Comparison function *)
 
-  val eq : t -> t -> bool
+  val equal : t -> t -> bool
   (** Equality function *)
 
   (* val hash : t -> int *)
@@ -32,39 +35,58 @@ sig
       module path. *)
 
   val pr : t -> Pp.std_ppcmds
+  (** Pretty-printing *)
 end
 
 type universe_level = Level.t
 (** Alias name. *)
 
+(** Sets of universe levels *)
 module LSet : 
 sig 
   include Set.S with type elt = universe_level
 	      
   val pr : t -> Pp.std_ppcmds
+  (** Pretty-printing *)
 end
 
 type universe_set = LSet.t
 
+(** Polymorphic maps from universe levels to 'a *)
 module LMap : 
 sig
   include Map.S with type key = universe_level
 
-  (** Favorizes the bindings in the first map. *)
   val union : 'a t -> 'a t -> 'a t
+  (** [union x y] favors the bindings in the first map. *)
+
   val diff : 'a t -> 'a t -> 'a t
+  (** [diff x y] removes bindings from x that appear in y (whatever the value). *)
 
   val subst_union : 'a option t -> 'a option t -> 'a option t
+  (** [subst_union x y] favors the bindings of the first map that are [Some],
+      otherwise takes y's bindings. *)
 
   val elements : 'a t -> (universe_level * 'a) list
+  (** As an association list *)
+
   val of_list : (universe_level * 'a) list -> 'a t
+  (** From an association list *)
+
   val of_set : universe_set -> 'a -> 'a t
+  (** Associates the same value to all levels in the set *)
+
   val mem : universe_level -> 'a t -> bool
-  val universes : 'a t -> universe_set
+  (** Is there a binding for the level? *)
 
   val find_opt : universe_level -> 'a t -> 'a option
+  (** Find the value associated to the level, if any *)
+
+  val universes : 'a t -> universe_set
+  (** The domain of the map *)
 
   val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds
+  (** Pretty-printing *)
 end
 
 type 'a universe_map = 'a LMap.t
@@ -72,38 +94,51 @@ type 'a universe_map = 'a LMap.t
 module Universe :
 sig
   type t
-  (** Type of universes. A universe is defined as a set of constraints w.r.t.
-      other universes. *)
+  (** Type of universes. A universe is defined as a set of level expressions.
+      A level expression is built from levels and successors of level expressions, i.e.:
+      le ::= l + n, n \in N.
+
+      A universe is said atomic if it consists of a single level expression with
+      no increment, and algebraic otherwise (think the least upper bound of a set of
+      level expressions).
+  *)
 
   val compare : t -> t -> int
   (** Comparison function *)
 
-  val eq : t -> t -> bool
-  (** Equality function *)
+  val equal : t -> t -> bool
+  (** Equality function on formal universes *)
 
   (* val hash : t -> int *)
   (** Hash function *)
 
   val make : Level.t -> t
-  (** Create a constraint-free universe out of a given level. *)
+  (** Create a universe representing the given level. *)
 
   val pr : t -> Pp.std_ppcmds
+  (** Pretty-printing *)
 
   val level : t -> Level.t option
+  (** Try to get a level out of a universe, returns [None] if it
+      is an algebraic universe. *)
 
   val levels : t -> LSet.t
+  (** Get the levels inside the universe, forgetting about increments *)
 
-  val normalize : t -> t
-
-  (** The type of a universe *)
   val super : t -> t
+  (** The universe strictly above *)
     
-  (** The max of 2 universes *)
   val sup   : t -> t -> t
-
-  val type0m : t  (** image of Prop in the universes hierarchy *)
-  val type0 : t  (** image of Set in the universes hierarchy *)
-  val type1 : t  (** the universe of the type of Prop/Set *)
+  (** The l.u.b. of 2 universes *)
+
+  val type0m : t  
+  (** image of Prop in the universes hierarchy *)
+  
+  val type0 : t  
+  (** image of Set in the universes hierarchy *)
+  
+  val type1 : t 
+  (** the universe of the type of Prop/Set *)
 end
 
 type universe = Universe.t
@@ -127,11 +162,6 @@ val sup : universe -> universe -> universe
 val super : universe -> universe
 
 val universe_level : universe -> universe_level option
-val compare_levels : universe_level -> universe_level -> int
-val eq_levels : universe_level -> universe_level -> bool
-
-(** Equality of formal universe expressions. *)
-val equal_universes : universe -> universe -> bool
 
 (** {6 Graphs of universes. } *)
 
@@ -147,37 +177,10 @@ val empty_universes : universes
 
 (** The initial graph of universes: Prop < Set *)
 val initial_universes : universes
-val is_initial_universes : universes -> bool
-
-(** {6 Constraints. } *)
-
-type constraint_type = Lt | Le | Eq
-type univ_constraint = universe_level * constraint_type * universe_level
-
-module Constraint : sig
- include Set.S with type elt = univ_constraint
-end
 
-type constraints = Constraint.t
-
-val empty_constraint : constraints
-val union_constraint : constraints -> constraints -> constraints
-val eq_constraint : constraints -> constraints -> bool
-
-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
+val is_initial_universes : universes -> bool
 
-(** A value with universe constraints. *)
-type 'a constrained = 'a * constraints
+(** {6 Substitution} *)
 
 type universe_subst_fn = universe_level -> universe
 type universe_level_subst_fn = universe_level -> universe_level
@@ -188,35 +191,52 @@ type universe_level_subst = universe_level universe_map
 
 val level_subst_of : universe_subst_fn -> universe_level_subst_fn
 
+(** {6 Universe instances} *)
+
 module Instance : 
 sig
   type t
+  (** A universe instance represents a vector of argument universes
+      to a polymorphic definition (constant, inductive or constructor). *)
 
-  val hcons : t -> t
   val empty : t
   val is_empty : t -> bool
 
-  val eq : t -> t -> bool
-
   val of_array : Level.t array -> t
   val to_array : t -> Level.t array
 
-  (** Rely on physical equality of subterms only *)
+  val append : t -> t -> t
+  (** To concatenate two instances, used for discharge *)
+
+  val equal : t -> t -> bool
+  (** Equality (note: instances are hash-consed, this is O(1)) *)
+
+  val hcons : t -> t
+  (** Hash-consing. *)
+
+  val hash : t -> int
+  (** Hash value *)
+
+  val share : t -> t * int
+  (** Simultaneous hash-consing and hash-value computation *)
+
   val eqeq : t -> t -> bool
+  (** Rely on physical equality of subterms only *)
 
   val subst_fn : universe_level_subst_fn -> t -> t
+  (** Substitution by a level-to-level function. *)
+
   val subst : universe_level_subst -> t -> t
+  (** Substitution by a level-to-level function. *)
 
   val pr : t -> Pp.std_ppcmds
-
-  val append : t -> t -> t
+  (** Pretty-printing, no comments *)
 
   val levels : t -> LSet.t
-
-  val max_level : t -> int
+  (** The set of levels in the instance *)
 
   val check_eq : t check_function 
-
+  (** Check equality of instances w.r.t. a universe graph *)
 end
 
 type universe_instance = Instance.t
@@ -225,6 +245,25 @@ type 'a puniverses = 'a * universe_instance
 val out_punivs : 'a puniverses -> 'a
 val in_punivs : 'a -> 'a puniverses
 
+(** {6 Constraints. } *)
+
+type constraint_type = Lt | Le | Eq
+type univ_constraint = universe_level * constraint_type * universe_level
+
+module Constraint : sig
+ include Set.S with type elt = univ_constraint
+end
+
+type constraints = Constraint.t
+
+val empty_constraint : constraints
+val union_constraint : constraints -> constraints -> constraints
+val eq_constraint : constraints -> constraints -> bool
+
+(** A value with universe constraints. *)
+type 'a constrained = 'a * constraints
+
+
 (** A list of universes with universe constraints,
     representiong local universe variables and constraints *)
 
@@ -283,6 +322,26 @@ 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
 
@@ -405,7 +464,6 @@ val dump_universes :
 
 (** {6 Hash-consing } *)
 
-val hcons_univlevel : universe_level -> universe_level
 val hcons_univ : universe -> universe
 val hcons_constraints : constraints -> constraints
 val hcons_universe_set : universe_set -> universe_set
@@ -413,3 +471,10 @@ val hcons_universe_context : universe_context -> universe_context
 val hcons_universe_context_set : universe_context_set -> universe_context_set 
 
 (******)
+
+(* deprecated: use qualified names instead *)
+val compare_levels : universe_level -> universe_level -> int
+val eq_levels : universe_level -> universe_level -> bool
+
+(** deprecated: Equality of formal universe expressions. *)
+val equal_universes : universe -> universe -> bool
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 62ddeb182..8e623415e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -176,7 +176,7 @@ let rec eq_puniverses f (x,l1) (y,l2) cu =
   else raise NotConvertible
 
 and conv_universes l1 l2 cu =
-  if Univ.Instance.eq l1 l2 then cu else raise NotConvertible
+  if Univ.Instance.equal l1 l2 then cu else raise NotConvertible
 
 let rec conv_eq pb t1 t2 cu =
   if t1 == t2 then cu
diff --git a/library/universes.ml b/library/universes.ml
index 73a0b2b1c..b31aab198 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -191,7 +191,7 @@ module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap)
 
 let remove_trivial_constraints cst =
   Constraint.fold (fun (l,d,r as cstr) nontriv ->
-    if d != Lt && eq_levels l r then nontriv
+    if d != Lt && Univ.Level.equal l r then nontriv
     else if d == Le && is_type0m_univ (Univ.Universe.make l) then nontriv
     else Constraint.add cstr nontriv)
     cst Constraint.empty
@@ -318,7 +318,7 @@ let normalize_univ_variable ~find ~update =
   let rec aux cur =
     let b = find cur in
     let b' = subst_univs_universe aux b in
-      if Universe.eq b' b then b
+      if Universe.equal b' b then b
       else update cur b'
   in fun b -> try aux b with Not_found -> Universe.make b
 
@@ -329,14 +329,14 @@ let normalize_univ_variable_opt_subst ectx =
     | None -> raise Not_found
   in
   let update l b =
-    assert (match Universe.level b with Some l' -> not (Level.eq l l') | None -> true);
+    assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
     ectx := Univ.LMap.add l (Some b) !ectx; b
   in normalize_univ_variable ~find ~update
 
 let normalize_univ_variable_subst subst =
   let find l = Univ.LMap.find l !subst in
   let update l b =
-    assert (match Universe.level b with Some l' -> not (Level.eq l l') | None -> true);
+    assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true);
     subst := Univ.LMap.add l b !subst; b in
     normalize_univ_variable ~find ~update
 
@@ -391,7 +391,7 @@ let subst_univs_subst u l s =
 exception Found of Level.t
 let find_inst insts v =
   try LMap.iter (fun k (enf,alg,v') ->
-    if not alg && enf && Universe.eq v' v then raise (Found k))
+    if not alg && enf && Universe.equal v' v then raise (Found k))
 	insts; raise Not_found
   with Found l -> l
 
@@ -481,7 +481,7 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	  (* u is not algebraic but has no upper bounds,
 	     we instantiate it with its lower bound if it is a 
 	     different level, otherwise we keep it. *)
-	  if not (Level.eq l u) && not (LSet.mem l algs) then
+	  if not (Level.equal l u) && not (LSet.mem l algs) then
 	    (* if right = None then. Should check that u does not 
 	       have upper constraints that are not already in right *)
 	      instantiate_with_lbound u lbound false false acc
@@ -639,11 +639,11 @@ let restrict_universe_context (univs,csts) s =
   in (univs', csts')
 
 let is_prop_leq (l,d,r) =
-  Level.eq Level.prop l && d == Univ.Le
+  Level.equal Level.prop l && d == Univ.Le
 
 (* Prop < i <-> Set+1 <= i <-> Set < i *)
 let translate_cstr (l,d,r as cstr) =
-  if Level.eq Level.prop l && d == Univ.Lt then
+  if Level.equal Level.prop l && d == Univ.Lt then
     (Level.set, d, r)
   else cstr
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index f7b677a1e..d8f28150a 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -206,9 +206,7 @@ let oib_equal o1 o2 =
       match o1.mind_arity, o2.mind_arity with
       | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} ->
 	eq_constr c1 c2 && Sorts.equal s1 s2
-      | {mind_user_arity=c1; mind_sort=s1},
-	{mind_user_arity=c2; mind_sort=s2} ->
-	eq_constr c1 c2 && Sorts.equal s1 s2
+      | _ -> false
     end &&
     Array.equal Id.equal o1.mind_consnames o2.mind_consnames
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 9b12c5eb3..88958d014 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -420,7 +420,7 @@ type result =
 let destructurate_prop t =
   let c, args = decompose_app t in
   match kind_of_term c, args with
-    | _, [_;_;_] when eq_constr c (Universes.constr_of_global (build_coq_eq ())) -> Kapp (Eq,args)
+    | _, [_;_;_] when is_global (build_coq_eq ()) c -> Kapp (Eq,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_neq) -> Kapp (Neq,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zne) -> Kapp (Zne,args)
     | _, [_;_] when eq_constr c (Lazy.force coq_Zle) -> Kapp (Zle,args)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c7173c2d1..4254c8188 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -177,10 +177,12 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
         (match s, s' with
 	| Prop x, Prop y when x == y -> None
 	| Prop _, Type _ -> None
-	| Type x, Type y when Univ.Universe.eq x y -> None (* false *)
+	| Type x, Type y when Univ.Universe.equal x y -> None (* false *)
 	| _ -> subco ())
       | Prod (name, a, b), Prod (name', a', b') ->
-	  let name' = Name (Namegen.next_ident_away (Id.of_string "x") (Termops.ids_of_context env)) in
+	  let name' = 
+	    Name (Namegen.next_ident_away (Id.of_string "x") (Termops.ids_of_context env))
+	  in
 	  let env' = push_rel (name', None, a') env in
 	  let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 	    (* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ae16fbebe..ef93a827a 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -351,7 +351,7 @@ let process_universe_constraints univs postponed vars alg local cstrs =
   let normalize = Universes.normalize_universe_opt_subst vars in
   let rec unify_universes fo l d r local postponed =
     let l = normalize l and r = normalize r in
-      if Univ.Universe.eq l r then local, postponed 
+      if Univ.Universe.equal l r then local, postponed 
       else 
 	let varinfo x = 
 	  match Univ.Universe.level x with
@@ -974,7 +974,7 @@ let make_flexible_variable evd b u =
     if b then
       let uu = Univ.Universe.make u in
       let substu_not_alg u' v =
-	Option.cata (fun vu -> Univ.Universe.eq uu vu && not (Univ.LSet.mem u' avars)) false v
+	Option.cata (fun vu -> Univ.Universe.equal uu vu && not (Univ.LSet.mem u' avars)) false v
       in
 	if not (Univ.LMap.exists substu_not_alg uvars)
 	then Univ.LSet.add u avars else avars 
@@ -1027,7 +1027,7 @@ let is_eq_sort s1 s2 =
   else
     let u1 = univ_of_sort s1
     and u2 = univ_of_sort s2 in
-      if Univ.Universe.eq u1 u2 then None
+      if Univ.Universe.equal u1 u2 then None
       else Some (u1, u2)
 
 let is_univ_var_or_set u = 
@@ -1083,7 +1083,7 @@ let has_lub evd u1 u2 =
   (* let normalize = Universes.normalize_universe_opt_subst (ref univs.uctx_univ_variables) in *)
   (* (\* let dref, norm = memo_normalize_universe d in *\) *)
   (* let u1 = normalize u1 and u2 = normalize u2 in *)
-    if Univ.Universe.eq u1 u2 then evd
+    if Univ.Universe.equal u1 u2 then evd
     else add_universe_constraints evd
       (Univ.UniverseConstraints.singleton (u1,Univ.ULub,u2))
 
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 634ff7d63..52ae56e2b 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -617,7 +617,7 @@ Section Basics.
  rewrite <- app_comm_cons; f_equal.
  rewrite IHn; [ | omega].
  rewrite removelast_app.
- f_equal.
+ apply f_equal.
  replace (size-n)%nat with (S (size - S n))%nat by omega.
  rewrite removelast_firstn; auto.
  rewrite i2l_length; omega.
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 158e45240..3b33a9184 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -393,7 +393,7 @@ let get_body subst obl =
   match obl.obl_body with
   | None -> assert false
   | Some (DefinedObl c) -> 
-    let _, ctx = Environ.constant_type_in_ctx (Global.env ()) c in
+    let ctx = Environ.constant_context (Global.env ()) c in
     let pc = subst_univs_fn_puniverses (Univ.level_subst_of subst) (c, Univ.UContext.instance ctx) in
       DefinedObl pc
   | Some (TermObl c) ->