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/vconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/vconv.ml') diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 62ddeb182..8e623415e 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -176,7 +176,7 @@ let rec eq_puniverses f (x,l1) (y,l2) cu = else raise NotConvertible and conv_universes l1 l2 cu = - if Univ.Instance.eq l1 l2 then cu else raise NotConvertible + if Univ.Instance.equal l1 l2 then cu else raise NotConvertible let rec conv_eq pb t1 t2 cu = if t1 == t2 then cu -- cgit v1.2.3