diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-06 22:46:21 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-11-06 22:46:21 +0000 |
| commit | 81b999ef75c38799b056de9b5dd93b3b6c6ea6d4 (patch) | |
| tree | d04dd3d48c59206b0c3b52448c437519ced8d1d0 /theories/Lists/List.v | |
| parent | 556df3bfae8a80563f9415199fa8651666eb1932 (diff) | |
small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is
more general.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10295 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Lists/List.v')
| -rw-r--r-- | theories/Lists/List.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Lists/List.v b/theories/Lists/List.v index c618257b9..d0bf5bee9 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -919,7 +919,7 @@ Section ListOps. apply perm_trans with (l1'++a::l2); auto using Permutation_cons_app. apply perm_skip. apply (IH a l1' l2 l3' l4); auto. - (* swap *) + (* contradict *) intros x y l l' Hp IH; intros. break_list l1 b l1' H; break_list l3 c l3' H0. auto. @@ -1692,8 +1692,8 @@ Section ReDun. inversion_clear 1; auto. inversion_clear 1. constructor. - swap H0. - apply in_or_app; destruct (in_app_or _ _ _ H); simpl; tauto. + contradict H0. + apply in_or_app; destruct (in_app_or _ _ _ H0); simpl; tauto. apply IHl with a0; auto. Qed. @@ -1702,8 +1702,8 @@ Section ReDun. induction l; simpl. inversion_clear 1; auto. inversion_clear 1. - swap H0. - destruct H. + contradict H0. + destruct H0. subst a0. apply in_or_app; right; red; auto. destruct (IHl _ _ H1); auto. |