diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-19 08:33:55 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-19 09:09:37 +0100 |
| commit | c3e26fca1d077a2b69926df85d05e067882c40b0 (patch) | |
| tree | 4bb0c1915307b2d4f58bb37b9438275a310297aa /kernel/entries.ml | |
| parent | 25f09e86ba1a3ab3c24d5e17336b01315a205e00 (diff) | |
Specific type for section definition entries.
This allows to statically ensure well-formedness properties.
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index ca79de404..35a158682 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -81,6 +81,14 @@ type 'a definition_entry = { const_entry_opaque : bool; const_entry_inline_code : bool } +type section_def_entry = { + secdef_body : constr Univ.in_universe_context_set Future.computation; + secdef_secctx : Context.Named.t option; + secdef_feedback : Stateid.t option; + secdef_type : types option; + secdef_universes : constant_universes_entry; +} + type inline = int option (* inlining level, None for no inlining *) type parameter_entry = |