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.
Fix (somewhat obsolete) [Existential] command, which conflicted with the shelf.

When an evar was instantiated it failed to disapear from the shelf. It had the consequence of stopping Qed from happening.

Fixes test-suite/success/apply.v
fix compilation on ocaml 3.12 (Close: 3833)
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 in a section disappear at its end, No modifier survives
  the section and is preserved as a module-level No modifier, and
  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.