diff options
Diffstat (limited to 'toplevel/autoinstance.ml')
| -rw-r--r-- | toplevel/autoinstance.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index af1330a42b..7027b89eec 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -181,6 +181,7 @@ let declare_record_instance gr ctx params = let def = deep_refresh_universes def in let ce = { const_entry_body=def; const_entry_type=None; + const_entry_polymorphic = true; const_entry_opaque=false } in let cst = Declare.declare_constant ident (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in @@ -196,6 +197,7 @@ let declare_class_instance gr ctx params = let ce = Entries.DefinitionEntry { const_entry_type=Some typ; const_entry_body=def; + const_entry_polymorphic=true; const_entry_opaque=false } in try let cst = Declare.declare_constant ident |