aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-07-24 17:47:40 +0200
committerMatthieu Sozeau2014-07-24 17:47:40 +0200
commit31c1280a000c03c3a48ee697032d67e3e06af3fa (patch)
tree18a66206265e37b1312966ca25aa7f5ebc3c00da /kernel
parentae5ea0c9d5c0e9a39a50a2348b2b8f08938d5f5c (diff)
Fix misleading pretty-printing of information for non-universe-polymorphic
definitions.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions