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/obligations.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 'vernac/obligations.mli')
| -rw-r--r-- | vernac/obligations.mli | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/vernac/obligations.mli b/vernac/obligations.mli index a276f9f9a..9cbbf6082 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -12,23 +12,12 @@ open Evd open Names open Pp open Globnames -open Decl_kinds - -(** Forward declaration. *) -val declare_fix_ref : (?opaque:bool -> definition_kind -> Univ.universe_context -> Id.t -> - Safe_typing.private_constants Entries.proof_output -> types -> Impargs.manual_implicits -> global_reference) ref - -val declare_definition_ref : - (Id.t -> definition_kind -> - Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits - -> global_reference Lemmas.declaration_hook -> global_reference) ref (* This is a hack to make it possible for Obligations to craft a Qed * behind the scenes. The fix_exn the Stm attaches to the Future proof * is not available here, so we provide a side channel to get it *) val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t - val check_evars : env -> evar_map -> unit val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t |