Mod_typing
Main functions for translating module entries
translate_module
produces a module_body
out of a module_entry
. In the output fields:
mod_expr
is Abstract
for a MType
entry, or Algebraic
for MExpr
.mod_type_alg
is None
only for a MExpr
without explicit signature.val translate_module :
'a Conversion.universe_state ->
Environ.env ->
Names.ModPath.t ->
Entries.inline ->
Entries.module_entry ->
Declarations.module_body * 'a
translate_modtype
produces a module_type_body
whose mod_type_alg
cannot be None
(and of course mod_expr
is Abstract
).
val translate_modtype :
'a Conversion.universe_state ->
Environ.env ->
Names.ModPath.t ->
Entries.inline ->
Entries.module_type_entry ->
Declarations.module_type_body * 'a
From an already-translated (or interactive) implementation and an (optional) signature entry, produces a final module_body
val finalize_module :
'a Conversion.universe_state ->
Environ.env ->
Names.ModPath.t ->
(Declarations.module_signature * Mod_subst.delta_resolver) ->
(Entries.module_type_entry * Entries.inline) option ->
Declarations.module_body * 'a
translate_mse_incl
translate the mse of a module or module type given to an Include
val translate_mse_include :
bool ->
'a Conversion.universe_state ->
Environ.env ->
Names.ModPath.t ->
Entries.inline ->
Entries.module_struct_entry ->
Declarations.module_signature * unit * Mod_subst.delta_resolver * 'a