Better structure for Ltac pretyping environments.
Fix evarconv not applying eta when it used to. Fixes bug#3319.
Change internalization of primitive projections to allow parsing [p t] as
a primitive application only if all parameters of [p] are implicit, falling
back to the internalization of the eta-expanded version otherwise. This makes
apply [p] succeed even if its record argument is not implicit, ensuring better
compatibility.
Proofview.Refine: give the ability to add a store to the created evars.
Tactics: adds a new [guard_no_unifiable] primitive.

Fails if the focused goals contain unifiable subgoals. Meant to be used to replicate the behaviour or [apply] and such using the dependent-goal-producing [refine].
A set of simple apply tactics based on the refinement mechanism.

These are very simple minded apply-s I call [apply_arity]. They are given a head term and its type, and adds the appropriate number of arguments (from "with" bindings if available or new evars otherwise) according the the number of [forall] in the type (it does not do any type transformation). The resulting term is then refined.

These are useful tactics when we know precisely the number of arguments we want. For instance in tactics such as [constructor] or [reflexivity].

There are, as usual, a [apply] and [eapply] variant. I've also added the (more natural in the current implementation) variant I called [full_apply_arity] which generates its evars as dependent subgoals.
Use the new [*apply_arity] to define the [*constructor] tactics.