Registering strict implicit arguments systematically.
Experimenting always forcing convertibility on strict implicit arguments
in tactic unification.
Fixing Coq compilation.
Feedback: API cleaned up, documented and made user extensible
STM: put hooks in key events to let plugins customize the feedback

The default hook value is the one used by CoqIDE
TQueue: let reader be picky when popping an item

E.g. let a worker pick up only jobs he is able to deal with.
WorkerPool: API to move a worker from an active pool to a parking one

This lets me have a pool of active workers of a fixed size,
plus a parking area where workers that completed their job
can stay holding their state (and eventually one can ask them
to query such state afterwards).
AsyncTaskQueue: API to park a worker

Generalize the old model by letting one park a worker and
by letting the (parked) worker be picky about the tasks it
picks up.

The use of that is the following: a proof worker, while performing
its "main" task (building a proof term) computes all the intermediate
states but returns only its main result.  One can ask the worker
to hang around, and react to special tasks, like printing the
goals of an intermediate state.
STM: new API async_query

When async_proofs_always_delegate is on, park proof workers and
dispatch to them queries.  This flips the current way of printing
goals in PIDE base UIs: it is not the worker that prints all goals
while coomputing the states (and the dies), it is the UI that asks
for them when they are under the eyes of the user.
AsyncTaskQueue: parsin can also happen in the workers now
async_queries_* merged with async_proofs_*
better to always print the thread id
Fix test flags for fake_ide
typos
STM: hook called whenever a state is unreachable

Even indirectly, if it depends on another state that in turn failed.
FAQ: fix some broken urls
Reverting the following block of three commits:
- Registering strict implicit arguments systematically (35fc7d728168)
- Experimenting always forcing convertibility on strict implicit arguments (a1a6d7b99eef5e6)
- Fixing Coq compilation (894a3d16471)

Systematically computing strict implicit arguments can lead to big
computations, so I suspend this attempt, waiting for improved
computation of implicit arguments, or alternative heuristics going
toward having more conversion in rewrite.
Future: API for blocking futures
STM: if a-p-always-delegate fetch states from parked worker on edit-at

If the async-proofs-always-delegate is passed, workers are killed
only when the proof they computed is obsolete.  If one jumps back
to a state that was computed by the worker (and not the master) instead
of (re)computing such state in the master ask the worker to send it
back.
Tactic primitives: missing [advance] lead to spurious dangling goals.

Closes #3801.