- 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

2 files changed, 8 insertions, 6 deletions

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c7173c2d1a..4254c8188b 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 ae16fbebee..ef93a827a6 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))