diff options
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 5ab3b5c3fb..3eb0703803 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -45,6 +45,8 @@ type dir_path val dir_path_ord : dir_path -> dir_path -> int +val dir_path_eq : dir_path -> dir_path -> bool + (** 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 @@ -52,6 +54,8 @@ val repr_dirpath : dir_path -> module_ident list val empty_dirpath : dir_path +val is_empty_dirpath : dir_path -> bool + (** Printing of directory paths as ["coq_root.module.submodule"] *) val string_of_dirpath : dir_path -> string @@ -66,6 +70,8 @@ val pr_label : label -> Pp.std_ppcmds val label_of_id : identifier -> label val id_of_label : label -> identifier +val eq_label : label -> label -> bool + module Labset : Set.S with type elt = label module Labmap : Map.S with type key = label |