aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/declareDef.mli
Commit message (Collapse)AuthorAge
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* [vernac] Remove forward hooks from Obligations.Gravatar Emilio Jesus Gallego Arias2017-06-20
This was (once again) a spurious inter-dependency, that we solve by introducing a new module with the proper functionality. This helps in cleaning up the code. Note that no code was changed, other than removing the setting of the references.