diff options
| author | Pierre-Marie Pédrot | 2014-03-05 20:14:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-05 20:15:04 +0100 |
| commit | 4e5747adfd7b5c83cac2c4bb242d85fd3cb6fdd0 (patch) | |
| tree | eb1bc399ecbdd9e147839492f5418e70695d2198 /lib/hMap.mli | |
| parent | 450628742c1c5ef5391b0a16acfc99ad23205094 (diff) | |
Fixing previous commit. Forgot to include some code.
Diffstat (limited to 'lib/hMap.mli')
| -rw-r--r-- | lib/hMap.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/hMap.mli b/lib/hMap.mli index 4519ba316a..45b722fda0 100644 --- a/lib/hMap.mli +++ b/lib/hMap.mli @@ -10,7 +10,10 @@ module type HashedType = sig type t val compare : t -> t -> int + (** Total ordering *) val hash : t -> int + (** Hashing function compatible with [compare], i.e. [compare x y = 0] implies + [hash x = hash y]. *) end (** Hash maps are maps that take advantage of having a hash on keys. This is |