aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/hintdb_in_ltac_bis.v
Commit message (Collapse)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
In particular, this closes bug 2417.