Giving to "subst" a more natural semantic (fixing #4214) by using all

equalities in configurations like

x=y
x=z
===
P(x,y,z)

where it now produces

===
P(z,z,z)

In particular (equations are processed from most ancient to most recent).

Thanks to this, a "repeat subst" can just be a "subst" in List.v.

Incidentally: moved a nf_enter to enter in subst_one, since the latter
is normally called from other tactics having normalized evars.

0 files changed, 0 insertions, 0 deletions