Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Remove reference name type. | 2018-06-18 | |
* | [api] Remove Misctypes. | 2018-06-12 | |
* | Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <- | 2018-06-04 | |
|\ | |||
* \ | Merge PR #7657: Fix a couple typos in deprecation messages | 2018-06-04 | |
|\ \ | |||
| * | | Fix a couple typos in deprecation messages | 2018-05-31 | |
| | * | Refactor parsing rules for Hint Resolve -> and Hint Resolve <- | 2018-05-31 | |
| |/ | |||
* / | [notations] Split interpretation and parsing of notations | 2018-05-31 | |
|/ | |||
* | Merge PR #6969: [api] Remove functions deprecated in 8.8 | 2018-05-31 | |
|\ | |||
* | | Move interning the [hint_pattern] outside the Typeclasses hooks. | 2018-05-30 | |
| * | [api] Remove deprecated object from `Term` | 2018-05-30 | |
|/ | |||
* | [api] Make `vernac/` self-contained. | 2018-05-27 |