diff options
Diffstat (limited to 'toplevel/ind_tables.ml')
| -rw-r--r-- | toplevel/ind_tables.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index f039a6c40f..e03c3e9b59 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -128,7 +128,9 @@ let define internal id c = { const_entry_body = c; const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false }, + const_entry_opaque = false; + const_entry_inline_code = false + }, Decl_kinds.IsDefinition Scheme) in (match internal with | KernelSilent -> () |