diff options
| author | Matthieu Sozeau | 2014-06-23 12:33:49 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-23 13:10:02 +0200 |
| commit | 7a68038054193f5e392d75d7f11eb8f272727d6b (patch) | |
| tree | 53bbecba9460c1fc0950c14c315800f0913ea83e /kernel/type_errors.ml | |
| parent | 9753da73ed9f1e12d16b7d9b66d0c68b1d015918 (diff) | |
The uses of the funext axiom forced levels to Set, relaxing its use doesn't.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions