Stm: smarter delegation policy

Stm used to delegate every proof when it was possible, but this may
be a bad idea.  Small proofs may take less time than the overhead
delegation implies (marshalling, etc...).

Now it delegates only proofs that take >= 1 second.

By default a proof takes 1 second (that may be wrong).

If the file was compiled before, it reuses the data stored in the .aux
file and assumes the timings are still valid.

After a proof is checked, Coq knows how long it takes for real, so it
wont predict it wrong again (when the user goes up and down in the
file for example).

CoqIDE now sends to Coq, as part of the init message, the file name
so that Coq can load the .aux file.
Extensions in the parser
GExt
What is missing is how reduce and type ...
typechecking without subst_P just compiling
Bug way of not having bytecode generation crash
GExt -> Ext translation
beginning of theories
it typechecks
all proofs are equals ?!
on the way to reduce isubst
isubst reduces
delta reduce to find an irrelevant proof
Explain the game rules
Cheat to get unification on arguments for free
Here is K
Reductionops machine reduces isubst (well the conversion test is too weak)