aboutsummaryrefslogtreecommitdiff
path: root/vernac/declareDef.ml
AgeCommit message (Collapse)Author
2017-06-20[vernac] Remove forward hooks from Obligations.Emilio Jesus Gallego Arias
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.