diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-30 11:48:40 -0400 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-10-30 12:06:14 -0400 |
| commit | 77cf18eb844b45776b2ec67be9f71e8dd4ca002c (patch) | |
| tree | ebdb8d21dbe412505e99985b4afef9078802b3a0 /stm/stm.mli | |
| parent | 8d99e4bf4c54e9eabb0910740f79375ff399b844 (diff) | |
Add a way to get the right fix_exn in external vernacular commands
involving Futures.
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 18ed6fc2e..0c05c93d4 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -136,3 +136,4 @@ val process_error_hook : Future.fix_exn Hook.t val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t +val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn) |