Pass Ltac2 variables in a dedicated environment for generic arguments.

This is a way to hack around the fact that various interpretation functions
rely wrongly on the values of the environment to do nasty tricks. Typically,
the interpretation of terms is broken, as it will fail when there is a bound
variable with the same name as a hypothesis, instead of producing the
hypothesis itself.

0 files changed, 0 insertions, 0 deletions