Rename eta_expand_ind_stacks, fix the one from the checker and adapt
it to the new representation of projections and the new mind_finite
type.
Fix parsing of "subterm(s)" strategy argument.
Adds an identifier context in pretying's Ltac context.

Binder names are interpreted as the Ltac specified one if available.
Ltac's [uconstr] values now use the identifier context to give names to binders.

It does not work fine for refine yet as, while the binder has indeed the correct name, the evars are pretyped in an environment with the Ltac name, hence goal do not display the appropriate name.
The pretyping of [uconstr] in [refine] uses the identifier of the ltac context for goal contexts.
Silence an ocaml warning.
Remove a redundant typing phase in the [refine] tactic.

The refined term is still typechecked twice (not counting Qed). But there seem to be a bug in the typechecker whereby it sometimes return terms which have universe inconsistencies. Until this is fixed, I'll leave the second typing phase which seems to catch these inconsistencies. To remove it, it suffices to change the [unsafe] flag to [true].
Fix checker/values.ml with latest changes due to projections and universes.
Retype terms resulting from the feeding of a context with a term.

Fixes bug #3455.
Fix checker treatment of inductives using subst_instances instead of subst_univs_levels.
Remove unused substitution functions in checker.
Fix checking of constants in checker. Prelude can now be checked.
Fix checker to handle projections with eta and universe polymorphism correctly.
Fix checker to handle projections with eta and universe polymorphism correctly,
simplifying conversion code.
Cleanup code for looking up projection bodies.
Remove debug printing code
Fix bug #3584, elaborating pattern-matching on primitive records to the
use of projections.
Renaming goal-entering functions.

1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals

This is more uniform with the other functions of Coq.
Fixing clearbody : typecheck definitions in context.
Adding a way to inject tactic closures in interpretation values.