diff options
| author | Emilio Jesus Gallego Arias | 2017-06-11 06:54:07 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-20 11:21:30 +0200 |
| commit | ec8523065abfb68aff9bd3664869224419885385 (patch) | |
| tree | 0d5d3397e52704baefbb273807a61a3cc81f6340 /kernel/type_errors.mli | |
| parent | 21f8312738f324d1c55e4ed7c451b642c9da70e6 (diff) | |
[vernac] Remove forward hooks from Obligations.
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.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions