diff options
| author | Matthieu Sozeau | 2015-10-12 15:39:20 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-12 15:39:20 +0200 |
| commit | 50183ce7200d6059b4146c0cc4933aa524178c02 (patch) | |
| tree | ef81d73765af835dc3c90bbb20b12b98f4a5bc17 /kernel | |
| parent | b9a3925288af0cf3023c9a0073dc1eb295270de8 (diff) | |
Univs: be more restrictive for template polymorphic constants: only
direct aliases are ok, and indices should not be made polymorphic. Fixes NFix.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 5 | ||||
| -rw-r--r-- | kernel/typeops.ml | 14 |
2 files changed, 11 insertions, 8 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index a02d5e2055..1f8706652f 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -165,10 +165,7 @@ let rec make_subst env = (* to be greater than the level of the argument; this is probably *) (* a useless extra constraint *) let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in - if Univ.Universe.is_levels s then - make (cons_subst u s subst) (sign, exp, args) - else (* Cannot handle substitution by i+n universes. *) - make subst (sign, exp, args) + make (cons_subst u s subst) (sign, exp, args) | (na,None,t)::sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index fe82d85d5d..8895bae5da 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -134,10 +134,16 @@ let extract_context_levels env l = let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = let params, ccl = dest_prod_assum env t in match kind_of_term ccl with - | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) -> - let param_ccls = extract_context_levels env params in - let s = { template_param_levels = param_ccls; template_level = u} in - TemplateArity (params,s) + | Sort (Type u) -> + let ind, l = decompose_app (whd_betadeltaiota env c) in + if isInd ind && List.is_empty l then + let mis = lookup_mind_specif env (fst (destInd ind)) in + let nparams = Inductive.inductive_params mis in + let paramsl = CList.lastn nparams params in + let param_ccls = extract_context_levels env paramsl in + let s = { template_param_levels = param_ccls; template_level = u} in + TemplateArity (params,s) + else RegularArity t | _ -> RegularArity t |