diff options
| author | Pierre-Marie Pédrot | 2014-02-28 14:38:22 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-05 21:23:06 +0100 |
| commit | 073e4a3fc9748268c2b4e5549e54d894c6fe74cd (patch) | |
| tree | a85d9da44db40558eafe9302ac38e7d4a7c2c4f4 /kernel/names.mli | |
| parent | 4177c2380fcd92bca07c97993c21ffd230408eca (diff) | |
Lazily computed hash in KerName.t.
Diffstat (limited to 'kernel/names.mli')
| -rw-r--r-- | kernel/names.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/kernel/names.mli b/kernel/names.mli index 56b812fd0c..3b7de68d9c 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -289,11 +289,13 @@ sig module CanOrd : sig val compare : t -> t -> int val equal : t -> t -> bool + val hash : t -> int end module UserOrd : sig val compare : t -> t -> int val equal : t -> t -> bool + val hash : t -> int end val equal : t -> t -> bool |