STM: resilient on errors in non delegated proofs

This commits makes the concept of delegated and async more orthogonal.
A proof can be async but not delegated to a worker (if it is known
to be very small it is too much overhead to delegate to a worker).
A proof that is not async cannot be delegated to a worker.

An async proof that contains an error does not prevent Coq from continuing
the execution (interactive mode) and can be fixed without invalidating
the whole document (CoqIDE knows how to do that) even if it is processed
locally.  It used to be the case only for delegated proofs, now it worker
for all the proofs that can be in principle delegated (doing it or not
is an implementation detail, an optimization).

0 files changed, 0 insertions, 0 deletions