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.mli14
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 0c3fb2ba7..bc0e20205 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -36,14 +36,14 @@ val translate_mse :
env -> module_path option -> inline -> module_struct_entry ->
module_alg_expr translation
-(** [translate_mse_incl] translate the mse of a real module (no
- module type here) given to an Include *)
-
-val translate_mse_incl :
- env -> module_path -> inline -> module_struct_entry ->
- module_alg_expr translation
-
val finalize_module :
env -> module_path -> module_expression translation ->
(module_type_entry * inline) option ->
module_body
+
+(** [translate_mse_incl] translate the mse of a module or
+ module type given to an Include *)
+
+val translate_mse_incl :
+ bool -> env -> module_path -> inline -> module_struct_entry ->
+ module_alg_expr translation