From 857e82b2ca0d164242070599b66138cc431509c9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 1 May 2015 10:21:36 +0200 Subject: 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. --- theories/Lists/List.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Lists') 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. -- cgit v1.2.3