diff options
| author | Hugo Herbelin | 2015-02-10 21:54:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-02-10 21:56:06 +0100 |
| commit | 525c0e434e9b9472b6249bfd575659eb2dbec206 (patch) | |
| tree | 1e72d9ee4c7cf094507207555c625927709255ad /kernel/type_errors.mli | |
| parent | f804e681f1550e1c20b8ce5b83bc66c876fb3c99 (diff) | |
Fixing #4001 (missing type constraints when building return clause of match).
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions