From a8ee1bef887fbf14ffe1380152993b0db4298c98 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 9 May 2014 03:04:35 +0200 Subject: Reuse universe level substitutions for template polymorphism, fixing performance problem with hashconsing at the same time. This fixes bug# 3302. --- plugins/extraction/extraction.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/extraction.ml') diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0ddc7c006..cce6aff28 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -207,7 +207,7 @@ let oib_equal o1 o2 = | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} -> eq_constr c1 c2 && Sorts.equal s1 s2 | TemplateArity p1, TemplateArity p2 -> - let eq o1 o2 = Option.equal Univ.Universe.equal o1 o2 in + let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in List.equal eq p1.template_param_levels p2.template_param_levels && Univ.Universe.equal p1.template_level p2.template_level | _, _ -> false -- cgit v1.2.3