diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index ff918293b..476da3d0e 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -189,7 +189,8 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls let kn = try let cie = { - const_entry_body = proj; + const_entry_body = + Future.from_val (proj,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_opaque = false; @@ -293,7 +294,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let class_body = it_mkLambda_or_LetIn field params in let class_type = Option.map (fun ar -> it_mkProd_or_LetIn ar params) arity in let class_entry = - { const_entry_body = class_body; + { const_entry_body = + Future.from_val (class_body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = class_type; const_entry_opaque = false; @@ -306,7 +308,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls let proj_type = it_mkProd_or_LetIn (mkProd(Name (snd id), inst_type, lift 1 field)) params in let proj_body = it_mkLambda_or_LetIn (mkLambda (Name (snd id), inst_type, mkRel 1)) params in let proj_entry = - { const_entry_body = proj_body; + { const_entry_body = + Future.from_val (proj_body,Declareops.no_seff); const_entry_secctx = None; const_entry_type = Some proj_type; const_entry_opaque = false; |