aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/modintern.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/modintern.mli')
-rw-r--r--interp/modintern.mli11
1 files changed, 10 insertions, 1 deletions
diff --git a/interp/modintern.mli b/interp/modintern.mli
index a29480663..71a00c2fe 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -14,8 +14,17 @@ open Libnames
open Names
open Topconstr
+(** Module internalization errors *)
+
+type module_internalization_error =
+ | NotAModuleNorModtype of string
+ | IncorrectWithInModule
+ | IncorrectModuleApplication
+
+exception ModuleInternalizationError of module_internalization_error
+
(** Module expressions and module types are interpreted relatively to
- eventual functor or funsig arguments. *)
+ possible functor or functor signature arguments. *)
val interp_modtype : env -> module_ast -> module_struct_entry