diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 13 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 3 |
2 files changed, 12 insertions, 4 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index fcb45befa0..274561f0ca 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -135,6 +135,8 @@ let actualize_decl_level env lev t = let sign,s = dest_arity env t in mkArity (sign,lev) +let polymorphism_on_non_applied_parameters = false + (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) let rec make_subst env = function @@ -154,15 +156,18 @@ let rec make_subst env = function let s = sort_as_univ (snd (dest_arity env a)) in let ctx,subst = make_subst env (sign, exp, args) in d::ctx, cons_subst u s subst - | (na,None,t)::sign, Some u::exp, [] -> + | (na,None,t as d)::sign, Some u::exp, [] -> (* No more argument here: we instantiate the type with a fresh level *) (* which is first propagated to the corresponding premise in the arity *) (* (actualize_decl_level), then to the conclusion of the arity (via *) (* the substitution) *) - let s = fresh_local_univ () in - let t = actualize_decl_level env (Type s) t in let ctx,subst = make_subst env (sign, exp, []) in - (na,None,t)::ctx, cons_subst u s subst + if polymorphism_on_non_applied_parameters then + let s = fresh_local_univ () in + let t = actualize_decl_level env (Type s) t in + (na,None,t)::ctx, cons_subst u s subst + else + d::ctx, subst | sign, [], _ -> (* Uniform parameters are exhausted *) sign,[] diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index d834504ab6..8b0f45ac9c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,7 +24,10 @@ open Typeops let constrain_type env j cst1 = function | None -> +(* To have definitions in Type polymorphic make_polymorphic_if_arity env j.uj_type, cst1 +*) + NonPolymorphicType j.uj_type, cst1 | Some t -> let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in |