aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.ml
Commit message (Expand)AuthorAge
...
* Cleaning up the implementation of search entries in Hints.Gravatar Pierre-Marie Pédrot2015-04-14
* Opaque implementation of auto tactics.Gravatar Pierre-Marie Pédrot2015-04-14
* More documented representation of hint objects.Gravatar Pierre-Marie Pédrot2015-04-13
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
* Update headers.Gravatar Maxime Dénès2015-01-12
* 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