diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 4 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 5 | ||||
| -rw-r--r-- | kernel/typeops.ml | 4 | ||||
| -rw-r--r-- | kernel/typeops.mli | 3 |
4 files changed, 8 insertions, 8 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index cc5beb974..a5cda5d13 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -129,6 +129,8 @@ let cook_constant env r = | PolymorphicArity (ctx,s) -> let t = mkArity (ctx,Type s.poly_level) in let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in - Typeops.make_polymorphic_if_arity env typ in + let j = make_judge (force (Option.get body)) typ in + Typeops.make_polymorphic_if_constant_for_ind env j + in let boxed = Cemitcodes.is_boxed cb.const_body_code in (body, typ, cb.const_constraints, cb.const_opaque, boxed,false) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index aedc44ac8..2b28a7147 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -24,10 +24,7 @@ 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 + make_polymorphic_if_constant_for_ind env j, cst1 | Some t -> let (tj,cst2) = infer_type env t in let (_,cst3) = judge_of_cast env j DEFAULTcast tj in diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 616349ba0..53f230baa 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -135,10 +135,10 @@ let extract_context_levels env = List.fold_left (fun l (_,b,p) -> if b=None then extract_level env p::l else l) [] -let make_polymorphic_if_arity env t = +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) -> + | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) -> let param_ccls = extract_context_levels env params in let s = { poly_param_levels = param_ccls; poly_level = u} in PolymorphicArity (params,s) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index fe428230a..5bb0dee1d 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -105,5 +105,6 @@ val type_of_constant_knowing_parameters : env -> constant_type -> constr array -> types (* Make a type polymorphic if an arity *) -val make_polymorphic_if_arity : env -> types -> constant_type +val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> + constant_type |