Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 18 insertions, 28 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index d71b48f6..b726d0ec 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -1,43 +1,38 @@
 (************************************************************************)
 (*  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.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
 open Names
 open Univ
 open Term
 open Sign
-(*i*)
 
-(* This module defines the entry types for global declarations. This
+(** This module defines the entry types for global declarations. This
    information is entered in the environments. This includes global
    constants/axioms, mutual inductive definitions, modules and module
    types *)
 
 
-(*s Local entries *)
+(** {6 Local entries } *)
 
 type local_entry =
   | LocalDef of constr
   | LocalAssum of constr
 
 
-(*s Declaration of inductive types. *)
+(** {6 Declaration of inductive types. } *)
 
-(* Assume the following definition in concrete syntax:
-\begin{verbatim}
-Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
+(** Assume the following definition in concrete syntax:
+{v Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
 ...
-with      Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1 | ... | cpnp : Tpnp.
-\end{verbatim}
-then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
-[mind_entry_arity] is [Ai], defined in context [[[x1:X1;...;xn:Xn]];
+with      Ip (x1:X1) ... (xn:Xn) : Ap := cp1 : Tp1 | ... | cpnp : Tpnp. v}
+
+then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
+[mind_entry_arity] is [Ai], defined in context [x1:X1;...;xn:Xn];
 [mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]].
 *)
 
@@ -53,30 +48,25 @@ type mutual_inductive_entry = {
   mind_entry_params : (identifier * local_entry) list;
   mind_entry_inds : one_inductive_entry list }
 
-(*s Constants (Definition/Axiom) *)
+(** {6 Constants (Definition/Axiom) } *)
 
 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 parameter_entry = types * bool  (*inline flag*)
+type parameter_entry = section_context option * types * inline 
 
 type constant_entry =
   | DefinitionEntry of definition_entry
   | ParameterEntry of parameter_entry
 
-(*s Modules *)
-
-
-type specification_entry = 
-    SPEconst of constant_entry
-  | SPEmind of mutual_inductive_entry
-  | SPEmodule of module_entry
-  | SPEmodtype of module_struct_entry
+(** {6 Modules } *)
 
-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