aboutsummaryrefslogtreecommitdiff
path: root/test-suite/failure/proofirrelevance.v
AgeCommit message (Expand)Author
2006-10-27Check that sort-polymorphic inductive types is not too laxherbelin