Monomorphization (kernel)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15992 85f007b7-540e-0410-9357-904b9bb8a0f7

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