FinFun.v: results about injective/surjective/bijective fonctions over finite domains

 + Some extra results about NoDup, Fin.t, ...
Less dependencies in Omega.
Small optimizations in Closure:

1. Only apply last Zupdates
2. Better smartmap with state.
Tentative fixup for the previous commit. It seems I have broken something
nasty relating memory management triggering random segfaults. But this seemed
really unlikely...
fake_ide: ported to spawn
STM: be conservative w.r.t. proofs containing global side effects
STM: when a worker is canceled mark the proof as broken
STM: fix valid_id coming from Qed errors
Timeout and Set Default Timeout fixed (closes: #3229)
Made Pre_env.lazy_val opaque.
TC: honor the use_typeclasses flag in pretyping

The coercion code was not seeing such flag and always trying
to resolve type classes.  In particular open_contr is pretyped
without type classes.
fast correction of bug #3234
Removing non-marshallable data from the Agram constructor. Instead of
containing opaque grammar objects, it now contains a string representing
the entry. In order to recover the entry from the string, the former must
have been created with [Pcoq.create_generic_entry] or similar. This is
guaranteed for entries generated by ARGUMENT EXTEND, and must be done by
hand otherwise.

Some plugins were fixed accordingly.
[nanoPG]: emacs like copy/paste
CoqIDE: when coqtop misbehaves kill it properly (no zombie)
Optimization in kernel/vars.ml: directly allocate a fixed-size block in the
subst1 case.
More sharing in Logic, together with some code cleaning.
Fix grammatical mistake in error message (bug #3238)
Stack operations of Reductionops in Reductionops.Stack
app_node, stack, state printers