Do not abstract over the named variable in unsafe introduction tactic.

There is no point in doing that. The term being abstracted does not contain the
named variable y, as it is an evar of the form ?e{Var x_1, ... Var x_n, Rel 1}.
In practice it means that only the binding creation matters, the substitution
behaving as the identity, and ending up costing for nothing.

0 files changed, 0 insertions, 0 deletions