aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMatthieu Sozeau2018-03-08 07:23:03 -0300
committerMatthieu Sozeau2018-03-08 07:40:27 -0300
commitce87e338529f4dd174f1c870b83162bac6d2b9ae (patch)
treee6c3209639b0057fe1456cf9a8704e0990f1417c /dev
parentd3f88e4e3aaf346f88801737c9145fe114f4942b (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')
0 files changed, 0 insertions, 0 deletions