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 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'plugins/extraction')

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
 
-- 
cgit v1.2.3