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