diff options
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index c44a17df2a..36b75668b2 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -51,7 +51,7 @@ type mutual_inductive_entry = { (** Some (Some id): primitive record with id the binder name of the record in projections. Some None: non-primitive record *) - mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; @@ -81,6 +81,13 @@ type 'a definition_entry = { const_entry_opaque : bool; const_entry_inline_code : bool } +type section_def_entry = { + secdef_body : constr; + secdef_secctx : Context.Named.t option; + secdef_feedback : Stateid.t option; + secdef_type : types option; +} + type inline = int option (* inlining level, None for no inlining *) type parameter_entry = |