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