diff options
Diffstat (limited to 'toplevel/autoinstance.ml')
| -rw-r--r-- | toplevel/autoinstance.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 049d631bf..e9601c123 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -187,7 +187,7 @@ 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= Future.from_val (def,Declareops.no_seff); const_entry_secctx = None; const_entry_type=None; const_entry_opaque=false; @@ -204,9 +204,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_type= Some typ; + const_entry_body= Future.from_val (def,Declareops.no_seff); const_entry_secctx = None; - const_entry_body = def; const_entry_opaque = false; const_entry_inline_code = false } in try |