diff options
| author | Matthieu Sozeau | 2014-05-08 13:54:26 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-05-08 19:23:51 +0200 |
| commit | efa11b99cd42d8806645109d96720a4c0c83756c (patch) | |
| tree | eefeb0bf064f432ffe75cc12b166424d646387d1 /dev | |
| parent | b440899b0f07a23dfce69ae38b0a2b993cc6370c (diff) | |
Fix performance problem with unification in presence of universes (bug #3302) by considering
Type i a ground term even when "i" is a flexible universe variable, using the infer_conv
function to do the unification of universes.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions