aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorMatthieu Sozeau2015-11-04 12:52:35 -0500
committerMatthieu Sozeau2015-11-04 12:52:35 -0500
commit95a4fcf8cd36e29034e886682ed3a6e2914ce04f (patch)
tree408edac97bef6e69ab3503500a1220015110db52 /kernel
parentb30ca8ac9e0225e6505fea0004ea37e7649c9cb6 (diff)
Univs: compatibility with 8.4.
When refreshing a type variable, always use a rigid universe to force the most general universe constraint, as in 8.4.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions