CoqIDE: better messages
Arguments: warn only if no option is given (Close 3860)
Dyn: add API to check of two Dyn.t are ==

A Dyn.t boxes a type tag with the original object, so calling
== on the Dyn.t does not work, hence this extra API.
Global: export the name of the summary entry

In this way one can make surgery on the system states, like
checking if two frozen states have the same environment (i.e.
no running "abstract" in between)
Summary: more surgery functions

API to let one forge a frozen state out of another frozen state
plus some frozen bits
CThread: use a different type for thread friendly in_channels
Spawn: fix request of Gc statistics
TQueue: a way to unblock threads begin destroyed waiting on pop
WorkerPool: simpler fuctor and no more parking area
AsyncTaskQueue: simpler model (no parking area, continuation tasks)
STM: simplify state management

Thanks the the previous patchset a worker can be asked to send
back "light" version of the system states.  This is reasonably
efficient hence the idea of letting a worker hang around just to
hold system states for retrieval on demand is dropped.
STM: rename and simplify flags
CoqIDE: cleanup jobs window on worker death
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).
Future: blocking by default

This makes queries like Print or Extraction block and not
raise the error "the value is not ready".  This should make
CoqIDE work for every kind of script.