aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/hintdb_in_ltac_bis.v
Commit message (Expand)AuthorAge
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* Add test-suite files for hintdb variables in Ltac.Gravatar Théo Zimmermann2017-02-07