STM: move out a couple of submodules

These modules are not as reusable as one may want them to be, but
moving them out simplifies a little STM.
Stateid: export a Set module
STM: perspective (tell the scheduler what the user sees)
fix compilation with ocaml < 4
nanoPG: better copy/paste
Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it had
no particular purpose.
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.