aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.ml
Commit message (Expand)AuthorAge
* Removing the last Evd.diff from Hints.Gravatar Pierre-Marie Pédrot2014-10-27
* Forgotten hints.ml{,i} files in 38b34dfffcc.Gravatar Hugo Herbelin2014-10-08