diff options
| author | Pierre-Marie Pédrot | 2019-06-20 08:14:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-24 11:02:11 +0200 |
| commit | bbec0ea51b4dfef1ddb09a2f876323aa1547f643 (patch) | |
| tree | 137c8e3c1d5cb05815e393fdf024b11dfe517d77 /kernel/entries.ml | |
| parent | be3bba54e39a316ded975b7c5ac5723fed41aa88 (diff) | |
Dedicated type for opaque entries in the kernel.
Even more invariants can be enforced this way.
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 3f33df3f74..62aab7c391 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -77,6 +77,16 @@ type section_def_entry = { secdef_type : types option; } +type 'a opaque_entry = { + opaque_entry_body : 'a; + (* List of section variables *) + opaque_entry_secctx : Constr.named_context option; + (* State id on which the completion of type checking is reported *) + opaque_entry_feedback : Stateid.t option; + opaque_entry_type : types option; + opaque_entry_universes : universes_entry; + opaque_entry_inline_code : bool } + type inline = int option (* inlining level, None for no inlining *) type parameter_entry = @@ -90,7 +100,7 @@ type primitive_entry = { type 'a constant_entry = | DefinitionEntry of constr Univ.in_universe_context_set definition_entry - | OpaqueEntry of 'a const_entry_body definition_entry + | OpaqueEntry of 'a const_entry_body opaque_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry |