When pretyping [uconstr] closures, don't use the local Ltac variable environment.

A closure is supposedly closed: all the relevant Ltac variables should be then. The last field [ltac_genargs], if I'm not mistaken, is there to represent the Ltac variables which are bound but not to something which makes sense in a term. They should be irrelevant at this point, since the uconstr has already been interpreted and these checks are supposed to have happened. (though I'm not entirely sure they do, it can be an interesting exercise to try and make [uconstr] behave weirdly)

I'm not quite sure why it caused #3679, though. But it still seems to be solved.

0 files changed, 0 insertions, 0 deletions