aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_typing.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/mod_typing.mli')
-rw-r--r--kernel/mod_typing.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index eef16dd8f..1fadec2ad 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -18,7 +18,7 @@ open Mod_subst
val translate_module : env -> module_entry -> module_body
-val translate_struct_entry : env -> module_struct_entry ->
+val translate_struct_entry : env -> module_struct_entry ->
struct_expr_body * substitution
val add_modtype_constraints : env -> module_type_body -> env