diff options
| author | Hugo Herbelin | 2017-11-10 01:29:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-14 09:47:07 +0100 |
| commit | 952748b37f6cb6626353ba97910eac438f636beb (patch) | |
| tree | 0b57c38088214f06fc9cad33851861a625536942 /API/API.mli | |
| parent | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (diff) | |
Fixes #6129 (declaration of coercions made compatible with local definitions).
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions