diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 9697b0b8b..1b32d343e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -250,9 +250,9 @@ and module_implementation = | Struct of module_signature (** interactive body *) | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) -and module_body = +and 'a generic_module_body = { mod_mp : module_path; (** absolute path of the module *) - mod_expr : module_implementation; (** implementation *) + mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) mod_type_alg : module_expression option; (** algebraic type *) mod_constraints : Univ.ContextSet.t; (** @@ -269,13 +269,14 @@ and module_body = - [Module M : T. ... End M] then [mod_expr = Struct; mod_type_alg = Some T] And of course, all these situations may be functors or not. *) -(** A [module_type_body] is just a [module_body] with no - implementation ([mod_expr] always [Abstract]) and also - an empty [mod_retroknowledge]. Its [mod_type_alg] contains +and module_body = module_implementation generic_module_body + +(** A [module_type_body] is just a [module_body] with no implementation and + also an empty [mod_retroknowledge]. Its [mod_type_alg] contains the algebraic definition of this module type, or [None] if it has been built interactively. *) -and module_type_body = module_body +and module_type_body = unit generic_module_body (** Extra invariants : |