aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.mli
Commit message (Expand)AuthorAge
* Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
* Exporting the original unprocessed hint in the hint running function.Gravatar Pierre-Marie Pédrot2015-10-14
* Refine fix for handling of the universe contexts of hints, depending onGravatar Matthieu Sozeau2015-10-09
* Fix CFGV contrib: handling of global hints introducing global universes.Gravatar Matthieu Sozeau2015-10-09
* Fix bug #4354: interpret hints in the right env and sigma.Gravatar Matthieu Sozeau2015-10-06
* Rationalizing a bit the interface of Hints.Gravatar Pierre-Marie Pédrot2015-05-11
* Opaque implementation of auto tactics.Gravatar Pierre-Marie Pédrot2015-04-14
* Making the hint entry type opaque.Gravatar Pierre-Marie Pédrot2015-04-12
* Making the hints for the auto tactics private.Gravatar Pierre-Marie Pédrot2015-04-10
* Update headers.Gravatar Maxime Dénès2015-01-12
* Forgotten hints.ml{,i} files in 38b34dfffcc.Gravatar Hugo Herbelin2014-10-08