diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index ee190d350..86849cbbb 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -203,6 +203,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls try let cie = { const_entry_body = proj; + const_entry_secctx = None; const_entry_type = Some projtyp; const_entry_opaque = false } in let k = (DefinitionEntry cie,IsDefinition kind) in @@ -312,6 +313,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls 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_secctx = None; const_entry_type = class_type; const_entry_opaque = false } in @@ -323,6 +325,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls 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_secctx = None; const_entry_type = Some proj_type; const_entry_opaque = false } in |