aboutsummaryrefslogtreecommitdiff
path: root/tactics/hints.ml
AgeCommit message (Expand)Author
2014-10-27Removing the last Evd.diff from Hints.Pierre-Marie Pédrot
2014-10-08Forgotten hints.ml{,i} files in 38b34dfffcc.Hugo Herbelin