From ec8523065abfb68aff9bd3664869224419885385 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Jun 2017 06:54:07 +0200 Subject: [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. --- vernac/obligations.mli | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'vernac/obligations.mli') 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 -- cgit v1.2.3