Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <- | Pierre-Marie Pédrot | 2018-06-04 |
|\ | |||
* \ | Merge PR #7657: Fix a couple typos in deprecation messages | Pierre-Marie Pédrot | 2018-06-04 |
|\ \ | |||
| * | | Fix a couple typos in deprecation messages | Armaël Guéneau | 2018-05-31 |
| | * | Refactor parsing rules for Hint Resolve -> and Hint Resolve <- | Armaël Guéneau | 2018-05-31 |
| |/ | |||
* / | [notations] Split interpretation and parsing of notations | Emilio Jesus Gallego Arias | 2018-05-31 |
|/ | |||
* | Merge PR #6969: [api] Remove functions deprecated in 8.8 | Maxime Dénès | 2018-05-31 |
|\ | |||
* | | Move interning the [hint_pattern] outside the Typeclasses hooks. | Gaëtan Gilbert | 2018-05-30 |
| * | [api] Remove deprecated object from `Term` | Emilio Jesus Gallego Arias | 2018-05-30 |
|/ | |||
* | [api] Make `vernac/` self-contained. | Emilio Jesus Gallego Arias | 2018-05-27 |