diff options
Diffstat (limited to 'kernel/declarations.ml')
-rw-r--r-- | kernel/declarations.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 4308f9c1a..282dad0da 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -49,6 +49,8 @@ let force = force subst_mps let subst_constr_subst = subst_substituted +type inline = int option (* inlining level, None for no inlining *) + type constant_body = { const_hyps : section_context; (* New: younger hyp at top *) const_body : constr_substituted option; @@ -57,7 +59,7 @@ type constant_body = { (* const_type_code : Cemitcodes.to_patch; *) const_constraints : constraints; const_opaque : bool; - const_inline : bool} + const_inline : inline } (*s Inductive types (internal representation with redundant information). *) |