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
---
 kernel/closure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/closure.ml')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index fd3ab525e2..a1a9b54f71 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
-- 
cgit v1.2.3