diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/declare.ml b/library/declare.ml index 20e5bdddc5..5c10728436 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -186,6 +186,7 @@ let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds { Entries.const_entry_body = body; const_entry_type = types; const_entry_opaque = opaque; + const_entry_inline_code = false; const_entry_secctx = None } in declare_constant ~internal id |