Fix a bug in the naming of binders.

The ident closure was not propagated when pretying a [uconstr] coming from a [uconstr] closure. This bug had never been reported, as far as I'm aware.
Fix: when interpreting a identifier in pretying, use the Ltac identifier substitution at the right place.

I used to change [id] to its interpretation before calling [pretype_id]. But it's incorrect: we need to use the Ltac interpretation only when looking up the rel context (where it has been interpreted previously). It would not be to use the interpreted identifier to look up the named context or the Ltac context.
Ltac names in binders: some Ltac values can be seen both as terms and identifiers.

Fixes Ergo.
Fix timing of evar-normalisation  of goals in [Ftactic.nf_enter].

All goals were normalised up front, rather than normalised after the tactic acting on previous goal had the chance to solve some evars, which then appeared non-instantiated to tactics which do not work up to evar map (most of them).