[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.

0 files changed, 0 insertions, 0 deletions