diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index d0f2289dc4..1be251a503 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -49,7 +49,8 @@ type constant_body = { const_body_code : Cemitcodes.to_patch_substituted; (* const_type_code : Cemitcodes.to_patch; *) const_constraints : constraints; - const_opaque : bool } + const_opaque : bool; + const_inline : bool} (*s Inductive types (internal representation with redundant information). *) @@ -202,7 +203,8 @@ let subst_const_body sub cb = { const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code; (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*) const_constraints = cb.const_constraints; - const_opaque = cb.const_opaque } + const_opaque = cb.const_opaque; + const_inline = cb.const_inline} let subst_arity sub = function | Monomorphic s -> |