aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declaremods.mli
diff options
context:
space:
mode:
Diffstat (limited to 'library/declaremods.mli')
-rw-r--r--library/declaremods.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 5cda0d28d..4a037b005 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -100,7 +100,7 @@ val import_module : bool -> module_path -> unit
(* Include *)
val declare_include : (env -> 'struct_expr -> module_struct_entry) ->
- 'struct_expr -> bool -> unit
+ 'struct_expr -> bool -> bool -> unit
(*s [iter_all_segments] iterate over all segments, the modules'
segments first and then the current segment. Modules are presented