aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-10-08 14:58:11 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-10-08 14:59:21 +0200
commitd6ff0fcefa21bd2c6424627049b0f5e49ed4df12 (patch)
tree0b8b5c4fa34383e8cfbbdb5e06c6b47857f9e3db /lib
parent33d153a01f2814c6e5486c07257667254b91fa0c (diff)
Univs: fix bug #4161.
Retypecheck abstracted infered predicate to register the right universe constraints.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions