diff options
| author | Hugo Herbelin | 2015-05-01 10:21:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-05-01 10:39:27 +0200 |
| commit | 857e82b2ca0d164242070599b66138cc431509c9 (patch) | |
| tree | daeabc761c5710a1c4d156f8183b253c75bb80f9 /test-suite | |
| 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 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4214.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4214.v b/test-suite/bugs/closed/4214.v new file mode 100644 index 0000000000..cd53c898e9 --- /dev/null +++ b/test-suite/bugs/closed/4214.v @@ -0,0 +1,5 @@ +(* Check that subst uses all equations around *) +Goal forall A (a b c : A), b = a -> b = c -> a = c. +intros. +subst. +reflexivity. |