diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-05-01 10:21:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-05-01 10:39:27 +0200 |
| commit | 857e82b2ca0d164242070599b66138cc431509c9 (patch) | |
| tree | daeabc761c5710a1c4d156f8183b253c75bb80f9 /intf | |
| parent | 5fc6e3a9e8fdd81be83194bbd62093993ddd4b01 (diff) | |
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.
Diffstat (limited to 'intf')
0 files changed, 0 insertions, 0 deletions