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.
Changing the semantics of Local/Global typeclass instances. Now, instances
do not escape a module if it is not imported. In particular:

- In a section: Local/No modifier in a section disappear at its end, while
  Global is preserved as such (and acts as a module-level global).
- In a module: Local never escape a module, No modifier only gets
  active when the module is imported, and Global is active as soon as the
  module is required.

Stdlib should be adapted accordingly, by adding Global in front of all instances.

Global flag is here for compatibility and should be deprecated on the long run.
Adapting the stdlib, plugins & test-suite.

Still broken though, because of subclass instances.