Term: include a function to print terms

I find it very odd not to have a pretty printer for terms than can
be called from *everywhere*.  This commit sticks in Term a long spaghetti
to let Printer install a printing function.
STM: remove dead code
Call Evd.nf_constraints only on Univ Poly constants

When one generates a .vi file only the type is stocked.
When one completes a .vi the proof term is stocked but the
corresponding type is not changed:
- if one minimizes the constraints of the body, the minimization
  could find that 2 univs are equal and substitute one for the
  other in the body, but it should also apply the subst to the type
  orelse coqchk could fail
- also, a "retroactive" change of a type (making it stricter)
  invalidates what was type checked afterwards, so this operation
  clashes with the vi2vo compilation chain
Hence we enable this optimization only for universe polymorphic
constants that:
- are the ones that truly requires such optimization
- are never processed asynchronously, so the scenario above does
  not apply
STM: do not call process_error twice (Close: 3880)
coqchk: flush the pp buffer from time to time
new test for coqchk
Revert "Term: include a function to print terms"

Such printer is already in Termops

This reverts commit 5d6106a075b79abbb92b03bbca7b13a517cf4925.
universes_of_constant: do a proper set union of body and type univs

Before the union was performed as a UContext.t union, that
concatenates the instances arrays, while one wants to avoid
duplicates.

We also assert that polymorphic constants have all constraints
in the constant_body (field const_universes), since the extra body
univs (stored in the opaque tables) are just for regular constants
processed asynchronously.
include test-suite/coqchk in the summary log
proof_global: make it possible to call close_proof in a worker

Given that the proof state contains a callback (a terminator)
that is not sent (dropped by the ephemeron mechanism at marshall
time) de-referencing the ephemeron during this function makes it
impossible to call it in a worker.  Now the worker can call the
function and replace the terminator with a good one.
STM: module Pp is open
STM: fix processing of errors
STM: check with the kernel proof terms on the worker too

Before this commit the worker was sending back a proof term
as built by tactics.  The master receives the proof terms and
eventually (when one clicks on the gears in CoqIDE) check it
with the kernel.  This meant that errors like the ones produced
by the "fix" tactics were discovered very late.

Now a worker checks with its kernel the proof term before sending it
back.  The term is also checked by the master, eventually, but the
error is signaled early.
remove debug prints (leftover)
Proof using: call "clear" to remove from sight the vars not selected

As discussed on coqdev, clear is not perfect, Hints for trivial
using cleared section vars are still used.

But it is better than nothing I guess.
Call nf_constraints also when compiling directly to vo

After commit b46944e the system got way slower, hence the optimization
is relevant also for non polymorphic constants.  Putting it back now,
but we shall find something in between: an optimization that does
not clash with async proofs but that gives some performance improvement
over no optimization at all.
Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many section variable.

For some reason, the subproofs solved by [auto] had started using [Hfinjective] from the section context.
Proof using: do not clear letins (unless they use a cleared var)
Fixing bug #3632 for good.
Adding a small lightweight thread library.