diff options
| author | Emilio Jesus Gallego Arias | 2018-11-13 02:06:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-19 00:22:40 +0100 |
| commit | 758041989f29ed960eba8bf7fe0d232d3937db60 (patch) | |
| tree | 72249e96642c99c2ed15ac5dad9037382f60c52e /proofs/proofs.mllib | |
| parent | 25e989019f72bd435d84a1d495c7de25165556dd (diff) | |
[proof] Provide better control of "open proofs" exceptions.
This is inspired and an alternative to #8981. We consolidate the "open
proof" exception, allowing clients to explicitly capture it and
removing some ugly duplicated code in the way.
The `Solve Obligation tac` semantics are then tweaked as to removed
the wide-scope "catch-all" and indeed will now relay errors in `tac`
as it will only absorb tactics that don't error but fail to close the
goal such as `auto`. For the rest of the cases, we introduce a
warning, and may move to a full error in later releases.
We also remove an unnecessary `tclCOMPLETE` call to code that will
actually call `close_proof`. In this case, it is better to delegate
error management to the core function.
Some error messages have changed [as we consolidate two error paths]
so this PR may require adjustment in that area.
Diffstat (limited to 'proofs/proofs.mllib')
| -rw-r--r-- | proofs/proofs.mllib | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 197f71ca91..f9bb2c3d60 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -2,9 +2,9 @@ Miscprint Goal Evar_refiner Proof_type -Logic Refine Proof +Logic Goal_select Proof_bullet Proof_global |