diff options
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 4 |
1 files changed, 3 insertions, 1 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) |