diff options
Diffstat (limited to 'toplevel/autoinstance.ml')
| -rw-r--r-- | toplevel/autoinstance.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 7027b89eec..af1330a42b 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -181,7 +181,6 @@ 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 @@ -197,7 +196,6 @@ 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 |