aboutsummaryrefslogtreecommitdiff
path: root/tactics/hints.ml
AgeCommit message (Expand)Author
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-16Ensuring purity of datastructures in the API.Pierre-Marie Pédrot
2015-04-14Cleaning up the implementation of search entries in Hints.Pierre-Marie Pédrot
2015-04-14Opaque implementation of auto tactics.Pierre-Marie Pédrot
2015-04-13More documented representation of hint objects.Pierre-Marie Pédrot
2015-03-03Fix bug #3590, keeping evars that are not turned into named metas byMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-10-27Removing the last Evd.diff from Hints.Pierre-Marie Pédrot
2014-10-08Forgotten hints.ml{,i} files in 38b34dfffcc.Hugo Herbelin