diff options
| author | Matthieu Sozeau | 2014-05-09 03:04:35 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-09 03:04:35 +0200 |
| commit | a8ee1bef887fbf14ffe1380152993b0db4298c98 (patch) | |
| tree | 995334f35933d651f99aa9ea0c8c958fb9ca5d21 /pretyping/inductiveops.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 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 0b7cd89f25..e180c13465 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -465,7 +465,7 @@ let rec instantiate_universes env evdref scl is = function let s = (* Does the sort of parameter [u] appear in (or equal) the sort of inductive [is] ? *) - if univ_depends u is then + if univ_depends (Univ.Universe.make u) is then scl (* constrained sort: replace by scl *) else (* unconstriained sort: replace by fresh universe *) |