diff options
| author | Matthieu Sozeau | 2016-07-20 12:29:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-20 12:30:01 +0200 |
| commit | 21f7472e430917707ff02930a05e13251e1fff9d (patch) | |
| tree | 39c45c0117299add5e9d88ecc65782c4621fe7b4 /kernel/type_errors.ml | |
| parent | 522bcd72a567a3ae29162519a9a9736581367251 (diff) | |
Fix bug #4780: universe leak in letin_tac
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions