test for apply + TC resolution
CoqIDE: better error reporting for Qed on incomplete proof
STM: when an error occurs in a worker send back a bunch of states

In this way when the user fixes the script only a small part of
the broken proof has to be recomputed on master.  The density of
states sent back decreases as they get far from the error. I.e.
counting from the error, the worker sends back states at distance
0 1 2 3 5 7 10 14 19 26 35 47...