aboutsummaryrefslogtreecommitdiff
path: root/kernel/names.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/names.mli')
-rw-r--r--kernel/names.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli
index 177768cf43..d0efe2380e 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -84,6 +84,8 @@ type module_path =
| MPdot of module_path * label
(*i | MPapply of module_path * module_path in the future (maybe) i*)
+val check_bound_mp : module_path -> bool
+
val string_of_mp : module_path -> string
module MPset : Set.S with type elt = module_path