aboutsummaryrefslogtreecommitdiff
path: root/vernac/declareDef.mli
AgeCommit message (Expand)Author
2017-11-24Use Entries.constant_universes_entry more.Gaƫtan Gilbert
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-06-20[vernac] Remove forward hooks from Obligations.Emilio Jesus Gallego Arias