From fd2daea8c6f2ab36125964c4e085377fd2ebdde3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 20 Jun 2019 09:39:28 +0200
Subject: Code simplification for definition_entry type.

---
 kernel/entries.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3