diff options
Diffstat (limited to 'toplevel/autoinstance.ml')
| -rw-r--r-- | toplevel/autoinstance.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 79ae41c1d..9258a39fc 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -179,7 +179,8 @@ let declare_record_instance gr ctx params = let ident = make_instance_ident gr in let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in let def = deep_refresh_universes def in - let ce = { const_entry_body=def; + let ce = { const_entry_body= def; + const_entry_secctx = None; const_entry_type=None; const_entry_opaque=false } in let cst = Declare.declare_constant ident @@ -194,8 +195,9 @@ let declare_class_instance gr ctx params = let def = deep_refresh_universes def in let typ = deep_refresh_universes typ in let ce = Entries.DefinitionEntry - { const_entry_type=Some typ; - const_entry_body=def; + { const_entry_type = Some typ; + const_entry_secctx = None; + const_entry_body= def; const_entry_opaque=false } in try let cst = Declare.declare_constant ident |