diff options
| author | Matthieu Sozeau | 2016-05-27 14:02:39 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-29 11:52:52 +0200 |
| commit | d4cdb7e41844e1bb77bac9a7b9df423364b996e2 (patch) | |
| tree | 082d76f16f315acd7f5ef4d153dcd5960f05837a /kernel/type_errors.ml | |
| parent | 25ffe7f97a907d3508848c81c3e8dcc89559aadd (diff) | |
Univs: add source locations of levels
For better error messages. The API change is
backwards compatible, using a new optional argument.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions