diff options
| author | Matthieu Sozeau | 2014-06-23 12:25:32 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-23 13:10:02 +0200 |
| commit | 9753da73ed9f1e12d16b7d9b66d0c68b1d015918 (patch) | |
| tree | 12f1ce4fef52eddafc9fa9e6890532e306cf65c8 /kernel/type_errors.ml | |
| parent | 44b149ec1d220d38754545f18a39ef76a3be44b5 (diff) | |
The test-suite file couldn't typecheck as it rightly introduces a universe inconsistency.
One needs to use a universe level lower than eq's parameter for this to be consistent.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions