diff options
Diffstat (limited to 'kernel/entries.mli')
| -rw-r--r-- | kernel/entries.mli | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/kernel/entries.mli b/kernel/entries.mli index 3b7a2fd19..b78372c0e 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -67,16 +67,14 @@ type constant_entry = (** {6 Modules } *) -type module_struct_entry = - MSEident of module_path - | MSEfunctor of MBId.t * module_struct_entry * module_struct_entry - | MSEwith of module_struct_entry * with_declaration - | MSEapply of module_struct_entry * module_struct_entry - -and with_declaration = - With_Module of Id.t list * module_path - | With_Definition of Id.t list * constr - -and module_entry = - { mod_entry_type : module_struct_entry option; - mod_entry_expr : module_struct_entry option} +type module_struct_entry = Declarations.module_alg_expr + +type module_params_entry = + (MBId.t * module_struct_entry) list (** older first *) + +type module_type_entry = module_params_entry * module_struct_entry + +type module_entry = + | MType of module_params_entry * module_struct_entry + | MExpr of + module_params_entry * module_struct_entry * module_struct_entry option |