Module `Mod_typing`

val translate_module : 'a Reduction.universe_state -> Environ.env -> Names.ModPath.t -> Entries.inline -> Entries.module_entry -> Declarations.module_body * 'a

val translate_modtype : 'a Reduction.universe_state -> Environ.env -> Names.ModPath.t -> Entries.inline -> Entries.module_type_entry -> Declarations.module_type_body * 'a

type 'alg translation = Declarations.module_signature * 'alg * Mod_subst.delta_resolver * Univ.Constraints.t

val translate_mse : 'a Reduction.universe_state -> Environ.env -> Names.ModPath.t option -> Entries.inline -> Entries.module_struct_entry -> Declarations.module_signature * (Constr.t * Univ.AbstractContext.t option) Declarations.module_alg_expr * Mod_subst.delta_resolver * 'a

val finalize_module : 'a Reduction.universe_state -> Environ.env -> Names.ModPath.t -> (Declarations.module_signature * Declarations.module_expression option * Mod_subst.delta_resolver) -> (Entries.module_type_entry * Entries.inline) option -> Declarations.module_body * 'a

val translate_mse_include : bool -> 'a Reduction.universe_state -> Environ.env -> Names.ModPath.t -> Entries.inline -> Entries.module_struct_entry -> Declarations.module_signature * unit * Mod_subst.delta_resolver * 'a