aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Lists')
-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.