diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-04 12:52:35 -0500 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-04 12:52:35 -0500 |
| commit | 95a4fcf8cd36e29034e886682ed3a6e2914ce04f (patch) | |
| tree | 408edac97bef6e69ab3503500a1220015110db52 /test-suite/bugs/closed/3297.v | |
| parent | b30ca8ac9e0225e6505fea0004ea37e7649c9cb6 (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 'test-suite/bugs/closed/3297.v')
0 files changed, 0 insertions, 0 deletions