Moving some tactic code to the new engine.
Adding an interface to Eqdecide and putting the grammar rules in a dedicated
file.
test for apply + TC resolution
CoqIDE: better error reporting for Qed on incomplete proof
STM: when an error occurs in a worker send back a bunch of states

In this way when the user fixes the script only a small part of
the broken proof has to be recomputed on master.  The density of
states sent back decreases as they get far from the error. I.e.
counting from the error, the worker sends back states at distance
0 1 2 3 5 7 10 14 19 26 35 47...
Removing tactic compatibility layer from Inv.
Removing Tacmach compatibility layer in Inv.
Removing tactic compatibility layer in Equality.
Removing Tacmach compatibility layer in Equality.
Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.
Cosmetic changes in Equality.
Removing tactic compatibility layer from Eqdecide.
Define Tactics.bring_hyps in the new monad.
Newline on -slash warning in coqdep.
Lighter interface for creating refining tactics.
Using the new refine interface to define ML tactics.
Removing dead code in Tactics.
Removing the Change_evar refiner rule.
Fixing bug #2900 (evar/evar unif was supposed to be treated in
solve_simple_eqn but in case the second evar was hidden behind a
local variable, it arrived in evar_define and imitate, wrongly
assuming progress).
Propagating conversion_problem towards (postponed) evar/evar problems.
Incidentally simplifies where evar/evar problems are treated (in
evar_define and imitate rather than solve_simple_eqn).