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 | |
| 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')
| -rw-r--r-- | pretyping/evarutil.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 4 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index d6b18175b4..18c91c0e30 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -830,7 +830,7 @@ let get_template_constructor_type evdref (ind, i) n = | Some u :: l, Prod (na, t, t') -> let u' = evd_comb0 (new_univ_variable Evd.univ_flexible) evdref in (* evdref := set_leq_sort !evdref u'l (Type u); *) - let s = Univ.LMap.add (Option.get (Univ.Universe.level u)) + let s = Univ.LMap.add u (Option.get (Univ.Universe.level u')) Univ.LMap.empty in let dom = subst_univs_level_constr s t in (* let codom = subst_univs_level_constr s t' in *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7715691b0c..aa302bac6f 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -221,7 +221,7 @@ val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> (* val get_template_constructor_type : evar_map ref -> constructor -> int -> types *) val get_template_constructor_type : evar_map ref -> constructor -> int -> - (Univ.universe option list * types) + (Univ.universe_level option list * types) val get_template_inductive_type : evar_map ref -> inductive -> int -> - (Univ.universe option list * types) + (Univ.universe_level option list * types) 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 *) |