aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.ml
Commit message (Expand)AuthorAge
* Univs/(e)auto: fix bug #4450 polymorphic exact hintsGravatar Matthieu Sozeau2016-06-09
* Hints/Univs: fix bug #4628 anomaliesGravatar Matthieu Sozeau2016-05-23
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix bug #4433, removing hack on evars appearing in a pattern from aGravatar Matthieu Sozeau2015-11-19
* Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
* Fixing a loop in checking hints with holes.Gravatar Hugo Herbelin2015-10-24
* Merge hint lists instead of appending them. (Fix bug #3199)Gravatar Guillaume Melquiond2015-10-16
* 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
* Univs: fix evar_map handling in Hint processing.Gravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* 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-27 02:32:54 +0000