diff options
| author | Théo Zimmermann | 2020-04-20 16:18:01 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-20 16:18:01 +0200 |
| commit | 2618b5dab38c9a3c2322e886d0b46b67b5cecfbf (patch) | |
| tree | 1dcd570915b2897e40af219dfff36e3c3703ac00 /kernel/type_errors.ml | |
| parent | 51cc164e858433961acc166e83e69880700a89f1 (diff) | |
Move new iter_table function to Goptions.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions