diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index bb6696389..5c2bd5b0a 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -40,6 +40,8 @@ module ModIdmap : Map.S with type key = module_ident type dir_path +val dir_path_ord : dir_path -> dir_path -> int + (** Inner modules idents on top of list (to improve sharing). For instance: A.B.C is ["C";"B";"A"] *) val make_dirpath : module_ident list -> dir_path @@ -68,6 +70,8 @@ module Labmap : Map.S with type key = label type mod_bound_id +val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int + (** The first argument is a file name - to prevent conflict between different files *) |