summaryrefslogtreecommitdiff
path: root/kernel/entries.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-04-28 14:59:16 +0000
commit2c4a6b4efe55a2c6ca9ca7b185723e7909e57269 (patch)
treee1542c8adb83ff297284eefc23a2703461713d9b /kernel/entries.ml
parent514dce2dfe717e3ed2e37dce6467b56219d451c1 (diff)
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Merge commit 'upstream/8.0pl3+8.1alpha' into 8.0pl3+8.1alpha
Diffstat (limited to 'kernel/entries.ml')
-rw-r--r--kernel/entries.ml15
1 files changed, 8 insertions, 7 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml
index a3d3d336..56b198c3 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: entries.ml,v 1.3.8.2 2005/11/29 21:40:51 letouzey Exp $ i*)
+(*i $Id: entries.ml 8647 2006-03-18 15:33:09Z herbelin $ i*)
(*i*)
open Names
@@ -32,9 +32,9 @@ type local_entry =
(* Assume the following definition in concrete syntax:
\begin{verbatim}
-Inductive I1 [x1:X1;...;xn:Xn] : A1 := c11 : T11 | ... | c1n1 : T1n1
+Inductive I1 (x1:X1) ... (xn:Xn) : A1 := c11 : T11 | ... | c1n1 : T1n1
...
-with Ip [x1:X1;...;xn:Xn] : Ap := cp1 : Tp1 | ... | cpnp : Tpnp.
+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]];
@@ -42,7 +42,6 @@ then, in $i^{th}$ block, [mind_entry_params] is [[xn:Xn;...;x1:X1]];
*)
type one_inductive_entry = {
- mind_entry_params : (identifier * local_entry) list;
mind_entry_typename : identifier;
mind_entry_arity : constr;
mind_entry_consnames : identifier list;
@@ -51,6 +50,7 @@ type one_inductive_entry = {
type mutual_inductive_entry = {
mind_entry_record : bool;
mind_entry_finite : bool;
+ mind_entry_params : (identifier * local_entry) list;
mind_entry_inds : one_inductive_entry list }
@@ -59,7 +59,8 @@ type mutual_inductive_entry = {
type definition_entry = {
const_entry_body : constr;
const_entry_type : types option;
- const_entry_opaque : bool }
+ const_entry_opaque : bool;
+ const_entry_boxed : bool}
type parameter_entry = types
@@ -84,8 +85,8 @@ and module_type_entry =
and module_signature_entry = (label * specification_entry) list
and with_declaration =
- With_Module of identifier * module_path
- | With_Definition of identifier * constr
+ With_Module of identifier list * module_path
+ | With_Definition of identifier list * constr
and module_expr =
MEident of module_path