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