aboutsummaryrefslogtreecommitdiff
path: root/kernel/indtypes.ml
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-12-19 14:42:09 +0100
committerMatthieu Sozeau2015-01-05 16:39:47 +0100
commitba2ad4fdcfb7e56a71c5797b82644cc9a49dd18f (patch)
tree652977782be0e9049095b002f70baeb7ce6a4b45 /kernel/indtypes.ml
parentce2efc0e02c4d164d9206361c0a2de6123816d00 (diff)
In Show Universes, print universes before normalization.
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions