consider_remaining_unif_problems respects Conv_oracle
Fix test-suite 2255.v
Evarconv: exact_ise_stack looks to stack head before bodies or branches

the order of the inspection is a "random" choise but going back to the old
behavior makes the compilation of ssreflect/rat.v 5 times faster ...
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.
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...