diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-05-09 03:04:35 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-09 03:04:35 +0200 |
| commit | a8ee1bef887fbf14ffe1380152993b0db4298c98 (patch) | |
| tree | 995334f35933d651f99aa9ea0c8c958fb9ca5d21 /plugins/extraction/extraction.ml | |
| parent | 75137f9b8a3426749e30d754be2354687e13c087 (diff) | |
Reuse universe level substitutions for template polymorphism, fixing performance
problem with hashconsing at the same time. This fixes bug# 3302.
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |