From 1eaebf4ab7616b2be16b957736e80f1d6100eae0 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 9 May 2013 20:48:29 +0000
Subject: Use definition_entry to declare local definitions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16502 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/entries.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/entries.mli')

diff --git a/kernel/entries.mli b/kernel/entries.mli
index b2d65d3ed3..392a2cd84f 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -47,9 +47,10 @@ type mutual_inductive_entry = {
   mind_entry_inds : one_inductive_entry list }
 
 (** {6 Constants (Definition/Axiom) } *)
+type const_entry_body = constr
 
 type definition_entry = {
-  const_entry_body   : constr;
+  const_entry_body   : const_entry_body;
   const_entry_secctx : Context.section_context option;
   const_entry_type        : types option;
   const_entry_opaque      : bool;
-- 
cgit v1.2.3