| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-07-17 | Remove automatic formatting of ComHints. | Pierre-Marie Pédrot | |
| This is about the third time I try to kill this file but for some reason it is still here. | |||
| 2020-04-21 | [hints] Move and split Hint Declaration AST to vernac | Emilio Jesus Gallego Arias | |
| This moves the vernacular part of hints to `vernac`; in particular, it helps removing the declaration of constants as parts of the `tactic` folder. | |||
