aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/sideff.v
AgeCommit message (Expand)Author
2015-10-29Handle side-effects of Vernacular commands inside proofs better, so thatMatthieu Sozeau