aboutsummaryrefslogtreecommitdiff
path: root/kernel/indtypes.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-08-30 13:17:52 +0200
committerGaëtan Gilbert2018-09-13 15:05:57 +0200
commitfa4c0aab3eace78fe283f4630e4db5ed076d267e (patch)
treed457553eaaeb421e269a0e982d1e06d9ed87d0e6 /kernel/indtypes.ml
parenteb4171d50d340e19e87a7a592b3d9c0d48654337 (diff)
Add entry for universe polymorphism critical bug
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions