diff options
Diffstat (limited to 'kernel/names.mli')
| -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 82df07562..6f4ac9a53 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -53,6 +53,9 @@ sig type t = Name of Id.t | Anonymous (** A name is either undefined, either an identifier. *) + val compare : t -> t -> int + (** Comparison over names. *) + val equal : t -> t -> bool (** Equality over names. *) |