aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml/doubleTypeInference.mli
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-06-15 13:24:41 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-06-15 13:24:41 +0200
commit0a51137f7ff80afdcf216d85cd8be25a531bc39b (patch)
treeb8ce1197001e7d387c42bc48ae155313d0ec6956 /plugins/xml/doubleTypeInference.mli
parentdf6e64fd28e9ba8b12045768869c7f083a15e9c0 (diff)
- Fix xml plugin treatment of inductives.
- Move HoTT bug #30 to closed
Diffstat (limited to 'plugins/xml/doubleTypeInference.mli')
0 files changed, 0 insertions, 0 deletions