summaryrefslogtreecommitdiff
path: root/kernel/entries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/entries.ml')
-rw-r--r--kernel/entries.ml17
1 files changed, 8 insertions, 9 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml
index b6b09c64..938d1c60 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 10664 2008-03-14 11:27:37Z soubiran $ i*)
+(*i $Id$ i*)
(*i*)
open Names
@@ -62,34 +62,33 @@ type definition_entry = {
const_entry_opaque : bool;
const_entry_boxed : bool}
-type parameter_entry = types*bool
+(* type and the inlining flag *)
+type parameter_entry = types * bool
-type constant_entry =
+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
- | SPEalias of module_path
| SPEmodtype of module_struct_entry
-
+
and 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
| MSEapply of module_struct_entry * module_struct_entry
-and with_declaration =
+and with_declaration =
With_Module of identifier list * module_path
| With_Definition of identifier list * constr
-and module_structure = (label * specification_entry) list
-
-and module_entry =
+and module_entry =
{ mod_entry_type : module_struct_entry option;
mod_entry_expr : module_struct_entry option}