aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/declareDef.ml
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* 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