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 /theories | |
| 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 'theories')
| -rw-r--r-- | theories/Lists/List.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index ea07a8497..5819fbe5e 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -2202,7 +2202,7 @@ Section ForallPairs. Proof. induction 1. inversion 1. - simpl; destruct 1; destruct 1; repeat subst; auto. + simpl; destruct 1; destruct 1; subst; auto. right; left. apply -> Forall_forall; eauto. right; right. apply -> Forall_forall; eauto. Qed. |