diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-08 14:58:11 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-08 14:59:21 +0200 |
commit | d6ff0fcefa21bd2c6424627049b0f5e49ed4df12 (patch) | |
tree | 0b8b5c4fa34383e8cfbbdb5e06c6b47857f9e3db /grammar/q_constr.ml4 | |
parent | 33d153a01f2814c6e5486c07257667254b91fa0c (diff) |
Univs: fix bug #4161.
Retypecheck abstracted infered predicate to register the right
universe constraints.
Diffstat (limited to 'grammar/q_constr.ml4')
0 files changed, 0 insertions, 0 deletions