aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/InvalidDisjunctiveIntro.v
AgeCommit message (Expand)Author
2017-12-11Catch errors while coercing 'and' intro patternsTej Chajed