From 7dfb0fb915fa095f8af57e8bb5e4727ebb61304a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
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/declareops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index be6c18810..92a566b7c 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -195,6 +195,7 @@ let subst_regular_ind_arity sub s =
 
 let subst_template_ind_arity sub s = s
 
+(* FIXME records *)
 let subst_ind_arity =
   subst_decl_arity subst_regular_ind_arity subst_template_ind_arity
 
-- 
cgit v1.2.3