diff options
| author | Matthieu Sozeau | 2013-11-04 18:42:56 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-06 09:58:55 +0200 |
| commit | 7f59465dad8be7fa04b2e6b4ed0c49c38cd9e532 (patch) | |
| tree | 86c014810cfc19b1e30c0f9c12bfb85d77c2463c /kernel | |
| parent | ede4fa2f51bee0a425f68cd159178835a3af3ca6 (diff) | |
Reinstate hashconsing of instances, faster globally.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index f156e6028e..8047a36f48 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1556,8 +1556,6 @@ struct let h = !accu land 0x3FFFFFFF in (a, h) end - - let hcons x = x let empty = hcons [||] |