diff options
| author | Frédéric Besson | 2019-09-17 18:09:06 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2019-10-03 14:31:13 +0200 |
| commit | 65b89a6b06b5ff2e26883800702cda19d2d980df (patch) | |
| tree | 1c740c10f52d7ad08eb448eb093e42c0510f7c95 /kernel/nativelib.ml | |
| parent | 92a55bf800a34b5ec283ce0419cde98f3312c9b8 (diff) | |
Improved handling of micromega caches
- Specialised hash and equality functions.
Avoid collisions in extreme scenarios.
- Flags to disable the use of the caches.
fixes #10772
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions