diff options
| author | Matthieu Sozeau | 2018-03-08 07:23:03 -0300 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-03-08 07:40:27 -0300 |
| commit | ce87e338529f4dd174f1c870b83162bac6d2b9ae (patch) | |
| tree | e6c3209639b0057fe1456cf9a8704e0990f1417c /dev/base_include | |
| parent | d3f88e4e3aaf346f88801737c9145fe114f4942b (diff) | |
Leave cumul constructor universes as is during unif
if we cannot coerce one constructor type to the other. By invariant
they have a common supertype
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions
