diff options
| author | Matthieu Sozeau | 2014-07-24 17:47:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-24 17:47:40 +0200 |
| commit | 31c1280a000c03c3a48ee697032d67e3e06af3fa (patch) | |
| tree | 18a66206265e37b1312966ca25aa7f5ebc3c00da /kernel/type_errors.ml | |
| parent | ae5ea0c9d5c0e9a39a50a2348b2b8f08938d5f5c (diff) | |
Fix misleading pretty-printing of information for non-universe-polymorphic
definitions.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions