From 7dfb0fb915fa095f8af57e8bb5e4727ebb61304a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 3 Nov 2013 20:48:34 +0100
Subject: - 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
---
 plugins/extraction/extraction.ml | 4 +---
 plugins/omega/coq_omega.ml       | 2 +-
 2 files changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index f7b677a1e1..d8f28150a6 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 9b12c5eb38..88958d0143 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)
-- 
cgit v1.2.3