Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Adding unique identifiers to hints. | 2015-05-12 | ||
* | Rationalizing a bit the interface of Hints. | 2015-05-11 | ||
* | Remove almost all the uses of string concatenation when building error messages. | 2015-04-23 | ||
* | Ensuring purity of datastructures in the API. | 2015-04-16 | ||
* | Cleaning up the implementation of search entries in Hints. | 2015-04-14 | ||
* | Opaque implementation of auto tactics. | 2015-04-14 | ||
* | More documented representation of hint objects. | 2015-04-13 | ||
* | Fix bug #3590, keeping evars that are not turned into named metas by | 2015-03-03 | ||
* | Update headers. | 2015-01-12 | ||
* | Removing the last Evd.diff from Hints. | 2014-10-27 | ||
* | Forgotten hints.ml{,i} files in 38b34dfffcc. | 2014-10-08 |