An optimization on filtering evar instances with let-ins suggested by

inefficiency #4076.

In an evar context like this one

x:X, y:=f(x), z:Z(x,y) |- ?x : T(x,y,z)

with unification problem

a:A, b:=f(t(a)) |- ?x[x:=t(a);y:=b;z:=u(a,b)] = v(a,b,c)

we now keep y after filtering, iff the name b occurs effectively in
v(a,b,c), while before, we kept it as soon as its expansion f(t(a))
had free variables in v(a,b,c), which was more often, but useless
since the point in keeping a let-in in the instance is precisely to
reuse the name of the let-in while unifying with a right-hand side
which mentions this name.

0 files changed, 0 insertions, 0 deletions