diff options
| author | Matthieu Sozeau | 2016-05-30 23:52:58 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-29 11:52:52 +0200 |
| commit | c200c2b41e88dd7d4a1b9e90e0c35a7ed047309c (patch) | |
| tree | 1ff729200d9e587ace74d4b83611af4a69e6afdf /kernel/type_errors.ml | |
| parent | d4cdb7e41844e1bb77bac9a7b9df423364b996e2 (diff) | |
Univs: Fix bug #4726
When using Record and an explicit sort constraint, the
universe was wrongly made flexible and minimized.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions