aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/ltac_plus.v
AgeCommit message (Expand)Author
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2014-01-06Add a test suite file for Ltac's "+" tactical.Arnaud Spiwack