summaryrefslogtreecommitdiff
path: root/kernel/entries.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /kernel/entries.mli
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'kernel/entries.mli')
-rw-r--r--kernel/entries.mli46
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