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/classes.ml | |
| 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/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 007b70bc0..2e8ebb853 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -417,7 +417,7 @@ let context poly l = let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in let hook = Lemmas.mk_hook (fun _ gr -> gr) in - let _ = Command.declare_definition id decl entry [] [] hook in + let _ = DeclareDef.declare_definition id decl entry [] [] hook in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus |