aboutsummaryrefslogtreecommitdiff
path: root/tactics/hints.mli
AgeCommit message (Expand)Author
2015-05-11Rationalizing a bit the interface of Hints.Pierre-Marie Pédrot
2015-04-14Opaque implementation of auto tactics.Pierre-Marie Pédrot
2015-04-12Making the hint entry type opaque.Pierre-Marie Pédrot
2015-04-10Making the hints for the auto tactics private.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-08Forgotten hints.ml{,i} files in 38b34dfffcc.Hugo Herbelin