Adding a Print Strategy vernacular command. It allows to check the
transparent status of variables and constants.
Documenting the Print Strategy command.
Slightly more efficient Array.smartmap & related.
Missing equalities in Names-like structures.
Revert "Makefile: the initial build of grammar.cma is now directory-driven"

This reverts commit f694544d016b085b3cd10007b9f7716ae2c3b022.

This commit was wrong, since (at least) the highparsing part depends
on the toplevel directory. I still didn't had time to fix that, so
in the meantime let's revert it.
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.