diff options
| author | Matthieu Sozeau | 2016-07-20 12:29:13 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-07-20 18:45:17 +0200 |
| commit | 6f7156661b28063abce3de8053411ed6564d60f9 (patch) | |
| tree | 7d7b8489ad3ed69ff04c89e9ec383faba507223a /kernel/type_errors.ml | |
| parent | 9c4433c8def3db27527757fdb5d318eb14f97ce1 (diff) | |
Fix bug #4780: universe leak in letin_tac
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions