diff options
| author | Vincent Laporte | 2019-10-10 13:37:12 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-10-22 06:39:10 +0000 |
| commit | a357060331b8806fc2a493e2abc426109f9522a6 (patch) | |
| tree | 48970154f18f936c0f023900cb7eb1e972a1ad45 /kernel/nativecode.ml | |
| parent | 956889d99f58cc63544fca70d81c3242860c7222 (diff) | |
OrderedTypeEx: do not use “omega”
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions