diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 0191880d16..e75900cfa1 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -117,6 +117,11 @@ type module_path = | MPself of mod_self_id | MPdot of module_path * label +let rec check_bound_mp = function + | MPbound _ -> true + | MPdot(mp,_) ->check_bound_mp mp + | _ -> false + let rec string_of_mp = function | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")" | MPbound uid -> string_of_uid uid |