- 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, 2 insertions, 4 deletions

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)