diff options
| author | Gaëtan Gilbert | 2020-04-20 13:33:20 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-20 15:52:05 +0200 |
| commit | 51cc164e858433961acc166e83e69880700a89f1 (patch) | |
| tree | ffe04baec71c24cc918a3a936ab9bc4574e29f24 /kernel/nativecode.mli | |
| parent | 9de39626d925aa8ed0138fc5b90ee30ccf1ac4c1 (diff) | |
Use polymorphic record for Vernacentries.iter_table
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions