Univs: be more restrictive for template polymorphic constants: only

direct aliases are ok, and indices should not be made polymorphic. Fixes NFix.

1 files changed, 10 insertions, 4 deletions

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