aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-09-26 16:29:16 +0200
committerGaëtan Gilbert2018-10-01 12:56:00 +0200
commit58e1d0f2006f3243cbf7b57a9858f5119ffea666 (patch)
tree8f3147b07daa3d93e0f31c268eb2be4c0bee76fc /kernel/nativecode.ml
parent9134d94d42bafd38dfcc6a09a99edd554e636b55 (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.ml')
0 files changed, 0 insertions, 0 deletions