diff options
| author | Gaëtan Gilbert | 2018-09-26 16:29:16 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-01 12:56:00 +0200 |
| commit | 58e1d0f2006f3243cbf7b57a9858f5119ffea666 (patch) | |
| tree | 8f3147b07daa3d93e0f31c268eb2be4c0bee76fc /kernel/nativecode.mli | |
| parent | 9134d94d42bafd38dfcc6a09a99edd554e636b55 (diff) | |
Fix checker soundness bug with polymorphism capturing global univs
Followup for #8341.
Not making a test as that's too difficult with our current infrastructure.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions