diff options
| author | Hugo Herbelin | 2014-06-30 20:45:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-30 20:45:20 +0200 |
| commit | fa69f12babe7f04fbda9a22eaf76736a96f0fdea (patch) | |
| tree | cc6250719586805f0c58cacb854bf81a376ec62f /kernel/type_errors.ml | |
| parent | 26c8ce24a5dad0d54c6efbc7265a15f8d92dfb0b (diff) | |
Clarifying 'No such bound variable' message in apply, as suggested in #2387
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions