[uconstr]: use a closure instead of eager substitution.

This avoids relying on detyping. As Matthieu Sozeau pointed out to me, [understand∘detyping] has no reason to be the identity. This may create surprising behaviour some times (when a detyped term loses its relations to the current context, in particular in terms of universes), and downright incompatibilities in the case of refine.

As a bonus this should be a faster implementation of [uconstr] with a leaner memory profile.
Revert the change in Constrintern introduced by "Add a type of untyped term to Ltac's value."

It was commit 52247f50fa9aed83cc4a9a714b6b8f779479fd9b.

The closure in uconstr renders these changes (pertaining to substitution of ltac variables during internalisation) obsolete.