aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/declareDef.ml
Commit message (Expand)AuthorAge
* Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
* Use Entries.constant_universes_entry more.Gravatar Gaƫtan Gilbert2017-11-24
* [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