Report the proof state when an error occurs during a proof

[ciaran-matthew-dunne]

Errors raised during a proof now report the proof state. An unfinished proof at end and most subproof-count mismatches already print the goals, but a failing tactic prints nothing:

[foo.lp:12:2-6] Call to tactic "fail".

The state is now attached to every such error, in the err_desc field of Fatal (from #1290): the message is unchanged, and the state is printed uncolored after it.

[foo.lp:12:2-6] Call to tactic "fail".
Proof state before tactic application:
a: π A
b: π B
------------------------------------------------------------------------------
0. ?4: π A

A subproof-count mismatch is only detected after the tactic ran, so it reports the state before and after it:

[foo.lp:11:2-11] Missing subproofs (0 subproofs for 2 subgoals).
Proof state before tactic application:
0. ?1: Π n:N, π (Q n)
Proof state after tactic application:
0. ?5: π (Q z)
1. ?7: Π x0:N, π (Q x0) → π (Q (succ x0))

An unfinished proof at end reports the remaining goals under a Proof state: heading.

The state is attached in the outer Tactic.handle, below which tacticals catch their own errors, so failures swallowed by try/orelse are unaffected. The LSP server disables the attachment for tactic failures (Proof.state_on_error) since editors display the goals themselves. Tests: tests/proof_state.ml on three new KO fixtures.

[fblanqui]

Thanks @ciaran-matthew-dunne !