diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-11 06:54:07 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-20 11:21:30 +0200 |
| commit | ec8523065abfb68aff9bd3664869224419885385 (patch) | |
| tree | 0d5d3397e52704baefbb273807a61a3cc81f6340 /vernac/vernac.mllib | |
| 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 'vernac/vernac.mllib')
| -rw-r--r-- | vernac/vernac.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index d631fae8a..f74073e1f 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -8,6 +8,7 @@ Metasyntax Auto_ind_decl Search Indschemes +DeclareDef Obligations Command Classes |