diff options
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 8d8997a2b..f7ff2013b 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -105,8 +105,7 @@ let define id internal c t = (DefinitionEntry { const_entry_body = c; const_entry_type = t; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() }, + const_entry_opaque = false }, Decl_kinds.IsDefinition Scheme) in definition_message id; kn |