diff options
| author | Emilio Jesus Gallego Arias | 2020-05-15 03:14:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-11 20:06:31 +0200 |
| commit | 0e2897d33a7c07236a34b6ba3a7bb1bc6bb4bb65 (patch) | |
| tree | 1435b99ca2abfd763922f2413f02fb6bf90a419f /vernac/declare.mli | |
| parent | 55d1ea37042cf589d9aae7450806e42f5e571403 (diff) | |
[declare] Remove some unused `fix_exn`
In the current proof save path, the kernel can raise an exception when
checking a proof wrapped into a future.
However, in this case, the future itself will "fix" the produced
exception, with the mandatory handler set at the future's creation
time.
Thus, there is no need for the declare layer to mess with exceptions
anymore, if my logic is correct. Note that the `fix_exn` parameter to
the `Declare` API was not used anymore.
This undoes 77cf18eb844b45776b2ec67be9f71e8dd4ca002c which comes from
pre-github times, so unfortunately I didn't have access to the
discussion.
We need to be careful in `perform_buildp` as to catch the `Qed` error
and properly notify the STM about it with `State.exn_on`; this was
previously done by the declare layer using a hack [grabbing internal
state of the future, that the future itself was not using as it was
already forced], but we now do it in the caller in a more principled
way.
This has been tested in the case that tactics succeed but Qed fails
asynchronously.
Diffstat (limited to 'vernac/declare.mli')
| -rw-r--r-- | vernac/declare.mli | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/vernac/declare.mli b/vernac/declare.mli index ef4f8c4825..979bdd4334 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -305,13 +305,11 @@ val declare_definition -> ?inline:bool -> types:EConstr.t option -> body:EConstr.t - -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) -> Evd.evar_map -> GlobRef.t val declare_assumption - : ?fix_exn:(Exninfo.iexn -> Exninfo.iexn) - -> name:Id.t + : name:Id.t -> scope:locality -> hook:Hook.t option -> impargs:Impargs.manual_implicits @@ -495,11 +493,6 @@ val obl_substitution : val dependencies : Obligation.t array -> int -> Int.Set.t -(* 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) ref - end (** Creating high-level proofs with an associated constant *) |