Fix treatment of projections in Cst_stacks and unfolding behavior in evarconv.
Move eta-expansion after delta reduction in kernel reduction. This makes
it closer to evarconv/unification's behavior and it is less prone
to weird failures and successes in case of first-order unification
sending problems where the two terms have different types.
Work around issues with FO unification trying to unify terms of
potentially different types, resulting in ill-typed terms due to eta.
Projection expansion now fails gracefully on retyping errors.
The proper fix to unification, checking that the heads for FO
have unifiable types, is currently too strong, adding unnecessary universe
constraints, so it is disabled for now. It might be quite expensive
too also it's not noticeable on the stdlib.