diff options
Diffstat (limited to 'kernel/entries.mli')
| -rw-r--r-- | kernel/entries.mli | 46 |
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 |