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.mli12
1 files changed, 6 insertions, 6 deletions
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index f14d63be9..81974edfa 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -13,20 +13,20 @@ open Mod_subst
open Names
-val translate_module : env -> module_path -> bool -> module_entry
+val translate_module : env -> module_path -> inline -> module_entry
-> module_body
-val translate_module_type : env -> module_path -> bool -> module_struct_entry ->
+val translate_module_type : env -> module_path -> inline -> module_struct_entry ->
module_type_body
-val translate_struct_module_entry : env -> module_path -> bool -> module_struct_entry ->
+val translate_struct_module_entry : env -> module_path -> inline -> module_struct_entry ->
struct_expr_body * struct_expr_body * delta_resolver * Univ.constraints
-val translate_struct_type_entry : env -> bool -> module_struct_entry ->
+val translate_struct_type_entry : env -> inline -> module_struct_entry ->
struct_expr_body * struct_expr_body option * delta_resolver * module_path * Univ.constraints
-val translate_struct_include_module_entry : env -> module_path
- -> bool -> module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
+val translate_struct_include_module_entry : env -> module_path -> inline ->
+ module_struct_entry -> struct_expr_body * delta_resolver * Univ.constraints
val add_modtype_constraints : env -> module_type_body -> env