diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/names.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index f9fe89cde2..4b20b1c73a 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -124,6 +124,9 @@ sig val equal : t -> t -> bool (** Equality over labels *) + val compare : t -> t -> int + (** Comparison over labels. *) + val make : string -> t (** Create a label out of a string. *) |