aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.ml
Commit message (Expand)AuthorAge
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Adding an option Loose Hint Behavior to handle hints loaded but not imported.Gravatar Pierre-Marie Pédrot2015-05-12
* Adding unique identifiers to hints.Gravatar Pierre-Marie Pédrot2015-05-12
* Rationalizing a bit the interface of Hints.Gravatar Pierre-Marie Pédrot2015-05-11
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Ensuring purity of datastructures in the API.Gravatar Pierre-Marie Pédrot2015-04-16
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 18:12:43 +0000