From 50183ce7200d6059b4146c0cc4933aa524178c02 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 12 Oct 2015 15:39:20 +0200 Subject: Univs: be more restrictive for template polymorphic constants: only direct aliases are ok, and indices should not be made polymorphic. Fixes NFix. --- kernel/typeops.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'kernel/typeops.ml') diff --git a/kernel/typeops.ml b/kernel/typeops.ml index fe82d85d5..8895bae5d 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 -- cgit v1.2.3