diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index acc764028f..1f9f65b5cd 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -105,6 +105,7 @@ val label : kernel_name -> label val string_of_kn : kernel_name -> string val pr_kn : kernel_name -> Pp.std_ppcmds +val kn_ord : kernel_name -> kernel_name -> int module KNset : Set.S with type elt = kernel_name module KNpred : Predicate.S with type elt = kernel_name |