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/SetoidList.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/SetoidList.v')
| -rw-r--r-- | theories/Lists/SetoidList.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 301a09f25..6c4e76d82 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -293,7 +293,7 @@ Lemma NoDupA_split : forall l l' x, NoDupA (l++x::l') -> NoDupA (l++l'). Proof. induction l; simpl in *; inversion_clear 1; auto. constructor; eauto. - swap H0. + contradict H0. rewrite InA_app_iff in *; rewrite InA_cons; intuition. Qed. @@ -309,7 +309,7 @@ Proof. rewrite InA_app_iff in *; rewrite InA_cons; auto. apply H; auto. constructor. - swap H0. + contradict H0. rewrite InA_app_iff in *; rewrite InA_cons; intuition. eapply NoDupA_split; eauto. Qed. @@ -482,9 +482,9 @@ Proof. rewrite InA_app_iff in H0. split; intros. assert (~eqA a x). - swap H3; apply InA_eqA with a; auto. + contradict H3; apply InA_eqA with a; auto. assert (~eqA a y). - swap H8; eauto. + contradict H8; eauto. intuition. assert (eqA a x \/ InA a l) by intuition. destruct H8; auto. @@ -569,7 +569,7 @@ destruct H0; apply eqA_trans with a; auto. split. inversion_clear 1. split; auto. -swap n. +contradict n. apply eqA_trans with y; auto. rewrite (IHl x y) in H0; destruct H0; auto. destruct 1; inversion_clear H; auto. @@ -595,7 +595,7 @@ unfold equivlistA; intros. rewrite removeA_InA. split; intros. rewrite <- H0; split; auto. -swap H. +contradict H. apply InA_eqA with x0; auto. rewrite <- (H0 x0) in H1. destruct H1. |