diff options
| author | Gaëtan Gilbert | 2019-06-27 13:36:39 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-27 13:41:45 +0200 |
| commit | 5a532f2e00d0e3dca8d7079f067c79f2bb1b6b14 (patch) | |
| tree | 55913a55662e73353f360d90baa7eff6e59e3867 /kernel/entries.ml | |
| parent | b7c85c2ebe8375232719cd2d61e55daef9b4a358 (diff) | |
Kernel transparent definition entries have no body universes.
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index ca08ba485e..bc389e9fcf 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -57,17 +57,15 @@ type mutual_inductive_entry = { } (** {6 Constants (Definition/Axiom) } *) -type 'a proof_output = constr Univ.in_universe_context_set * 'a -type 'a const_entry_body = 'a proof_output Future.computation type definition_entry = { - const_entry_body : constr Univ.in_universe_context_set; + const_entry_body : constr; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; - const_entry_type : types option; - const_entry_universes : universes_entry; + const_entry_type : types option; + const_entry_universes : universes_entry; const_entry_inline_code : bool } type section_def_entry = { @@ -98,6 +96,9 @@ type primitive_entry = { prim_entry_content : CPrimitives.op_or_type; } +type 'a proof_output = constr Univ.in_universe_context_set * 'a +type 'a const_entry_body = 'a proof_output Future.computation + type 'a constant_entry = | DefinitionEntry of definition_entry | OpaqueEntry of 'a const_entry_body opaque_entry |