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 06446e2eb..d7121d6f6 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -125,7 +125,7 @@ val set_end_library_hook : (unit -> unit) -> unit
(** [really_import_module mp] opens the module [mp] (in a Caml sense).
It modifies Nametab and performs the [open_object] function for
- every object of the module. *)
+ every object of the module. Raises [Not_found] when [mp] is unknown. *)
val really_import_module : module_path -> unit