Ensuring the invariant that hypotheses and named context of the environment of
Proofview goals coincide by always using the named context and discarding the
hypotheses.
Only using filtered hyps in Goal.enter.

This was probably a bug. A user-side code should never be able to observe
the difference between filtered and unfiltered hypotheses.
At last a working clearbody!

This time it should work at least as well as the previous version. The error
messages were adapted a little. There is still a buggy behaviour when clearing
lets in section, but this is mostly a problem of section handling. The v8.4
version of clearbody did exhibit the same behaviour anyway.
Fix primitive projections declarations for inductive records.
Removing the old implementation of clear_body.
Adding a Ftactic module for potentially focussing tactics.

The code for the module was moved from Tacinterp. We still expose partially
the implementation of the Ftactic.t type, for the sake of simplicity. It may
be dangerous if used improperly though.
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.