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 /kernel/declareops.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 'kernel/declareops.ml')
| -rw-r--r-- | kernel/declareops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 55868097f..dd906bab2 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -31,8 +31,8 @@ let map_decl_arity f g = function | TemplateArity a -> TemplateArity (g a) let hcons_template_arity ar = - { template_param_levels = - List.smartmap (Option.smartmap Univ.hcons_univ) ar.template_param_levels; + { template_param_levels = ar.template_param_levels; + (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *) template_level = Univ.hcons_univ ar.template_level } (** {6 Constants } *) |