From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 kernel/entries.ml | 22 +++++++---------------
 1 file changed, 7 insertions(+), 15 deletions(-)

(limited to 'kernel/entries.ml')

diff --git a/kernel/entries.ml b/kernel/entries.ml
index 4ca21277..a4485fac 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: entries.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*i*)
 open Names
 open Univ
@@ -58,12 +56,13 @@ type mutual_inductive_entry = {
 
 type definition_entry = {
   const_entry_body   : constr;
+  const_entry_secctx : section_context option;
   const_entry_type   : types option;
-  const_entry_opaque : bool;
-  const_entry_boxed  : bool}
+  const_entry_opaque : bool }
+
+type inline = int option (* inlining level, None for no inlining *)
 
-(* type and the inlining flag *)
-type parameter_entry = types * bool
+type parameter_entry = section_context option * types * inline 
 
 type constant_entry =
   | DefinitionEntry of definition_entry
@@ -71,14 +70,7 @@ type constant_entry =
 
 (*s Modules *)
 
-
-type specification_entry = 
-    SPEconst of constant_entry
-  | SPEmind of mutual_inductive_entry
-  | SPEmodule of module_entry
-  | SPEmodtype of module_struct_entry
-      
-and module_struct_entry = 
+type module_struct_entry =
     MSEident of module_path
   | MSEfunctor of mod_bound_id * module_struct_entry * module_struct_entry
   | MSEwith of module_struct_entry * with_declaration
-- 
cgit v1.2.3