diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-02-10 11:07:10 +0100 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-15 20:45:29 +0100 |
| commit | 888d4be3ea2a45cff416fd8896276cfa8fc00518 (patch) | |
| tree | cdf0c5a856e29a9924a08fc961b29f6e59c56d45 /vernac/obligations.mli | |
| parent | 4db82417bdda1f9b0c7ea6ba9f6d71c03cc07eba (diff) | |
Make Obligations see fix_exn
Diffstat (limited to 'vernac/obligations.mli')
| -rw-r--r-- | vernac/obligations.mli | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 80b689144..11366fe91 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -24,6 +24,12 @@ val declare_definition_ref : 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 |