diff options
| author | whitequark | 2018-06-17 12:06:17 +0000 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-03 14:00:42 +0200 |
| commit | 326f52393f03b4255822f80ffaa52c4e585c8a61 (patch) | |
| tree | c8ae42c708a10a7d733fd19705f0aaa69ebf6a12 /kernel | |
| parent | 016f4a302090bcbb4ad47197dda2c60d6f598f6a (diff) | |
Rewrite CEphemeron to use a type-safe implementation based on GADTs.
This eliminates 2 uses of Obj from TCB.
Moreover, with the new implementation, a key that is marshalled
and then unmarshalled does not compare equal with itself even using
the polymorphic equality function.
See the comment in CEphemeron.ml for details on implementation.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions