aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/declareDef.ml
Commit message (Expand)AuthorAge
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* [vernac] Remove forward hooks from Obligations.Gravatar Emilio Jesus Gallego Arias2017-06-20