diff options
| author | Pierre-Marie Pédrot | 2019-06-20 09:39:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-24 11:02:11 +0200 |
| commit | fd2daea8c6f2ab36125964c4e085377fd2ebdde3 (patch) | |
| tree | e648694ecfc6453b8a508e2f37580640b3c412cc | |
| parent | 5de7daa41e677798e4169a3e6350af0df12017e8 (diff) | |
Code simplification for definition_entry type.
| -rw-r--r-- | kernel/entries.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index f73111d35f..2d29c3ee19 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -60,8 +60,8 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation -type 'a definition_entry = { - const_entry_body : 'a; +type definition_entry = { + const_entry_body : constr Univ.in_universe_context_set; (* List of section variables *) const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) @@ -99,7 +99,7 @@ type primitive_entry = { } type 'a constant_entry = - | DefinitionEntry of constr Univ.in_universe_context_set definition_entry + | DefinitionEntry of definition_entry | OpaqueEntry of 'a const_entry_body opaque_entry | ParameterEntry of parameter_entry | PrimitiveEntry of primitive_entry |