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.
Add a backtracking version of Ltac's [match].

[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.