STM: make -async-proofs on work from coqc too
STM: make the slave start from the most recent known state
Fixing checker with respect to new kernel name structure and hashmaps.
Some wrong generic equalities and hashes were removed too.
Printing backtraces in coqchk while in debug mode.
Remove the -fno-defer-pop cflag

According to http://caml.inria.fr/mantis/view.php?id=6346, this flag
causes ocamlc to fail on the latest version of xcode, because clang now
errors on -fno-defer-pop.  According to the same issue, -fno-defer-pop
is required for computed gotos if you're using gcc 1.xx, but not gcc
3.4.0 nor 4.4.7 (nor presumably other reasonably modern versions of
gcc).  I haven't actually tested this, as I don't have a mac, but it's a
relatively small change.

Signed-off-by: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
Adding phantom types to discriminate normalized goals, and adding a way to
observe non-normalized goals.
Using non-normalized goals in tactic interpretation.
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.