Updating to the new use of 3 universes, after Hurkens is simplified.
Fixing use of arguments renaming in apply which was broken after
reorganization of apply in d5fece25d8964d5d9fcd55b66164286aeef5fb9f:
using renaming also in retyping.
Fixing new failure of #3017 after 012fe1a96ba81ab (Referring to evars
by names): VarInstance behaves like GoalEvar for type class
resolution.
Going back on granting wish #1039 in f5d7b2b1e so that apply with
works correctly with an hypothesis of the context and knowing that
related bug #3204 had its own fix.
Made Tacsubst independent of Auto at linking time so that Tacenv does
not draw Auto.
Fixing nice printing of error reporting with ml tactics bound to ltac names.