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/inductive.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 64a6f1e17b..7cf5dd62dc 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -156,8 +156,8 @@ let sort_as_univ = function
 
 let cons_subst u su subst =
   try
-    (u, Universe.sup su (List.assoc_f Universe.eq u subst)) ::
-      List.remove_assoc_f Universe.eq u subst
+    (u, sup su (List.assoc_f Universe.equal u subst)) ::
+      List.remove_assoc_f Universe.equal u subst
   with Not_found -> (u, su) :: subst
 
 let actualize_decl_level env lev t =
-- 
cgit v1.2.3