aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Inductive.v
AgeCommit message (Expand)Author
2015-10-22Fixing a bug in reporting ill-formed inductive.Hugo Herbelin