Module Modintern

type module_internalization_error =
| NotAModuleNorModtype of Libnames.qualid
| NotAModuleType of Libnames.qualid
| NotAModule of Libnames.qualid
| IncorrectWithInModule
| IncorrectModuleApplication
exception ModuleInternalizationError of module_internalization_error
type module_kind =
| Module
| ModType
| ModAny
val intern_module_ast : module_kind -> Constrexpr.module_ast -> (Constrexpr.universe_decl_expr option * Constrexpr.constr_expr) Declarations.module_alg_expr * Names.ModPath.t * module_kind

Module internalization, i.e. from AST to module expression

val interp_module_ast : Environ.env -> module_kind -> Names.ModPath.t -> (Constrexpr.universe_decl_expr option * Constrexpr.constr_expr) Declarations.module_alg_expr -> Entries.module_struct_entry * Univ.ContextSet.t

Module interpretation, i.e. from module expression to typed module entry