diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 22cfd62a0c..7f7f7dcc39 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -47,7 +47,8 @@ type constant_body = { const_body_code : to_patch_substituted; (*i const_type_code : to_patch;i*) const_constraints : constraints; - const_opaque : bool } + const_opaque : bool; + const_inline : bool} val subst_const_body : substitution -> constant_body -> constant_body |