[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.

0 files changed, 0 insertions, 0 deletions