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/typeops.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/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c6355b3ea..49f883628 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -115,7 +115,7 @@ let check_hyps_inclusion env c sign = let extract_level env p = let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Some u | _ -> None + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None let extract_context_levels env l = let fold l (_, b, p) = match b with |