aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-05-01 10:21:36 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-05-01 10:39:27 +0200
commit857e82b2ca0d164242070599b66138cc431509c9 (patch)
treedaeabc761c5710a1c4d156f8183b253c75bb80f9 /theories
parent5fc6e3a9e8fdd81be83194bbd62093993ddd4b01 (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.v2
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.