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/FSets/FSetToFiniteSet.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/FSets/FSetToFiniteSet.v')
| -rw-r--r-- | theories/FSets/FSetToFiniteSet.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v index 747fd3796..de483f158 100644 --- a/theories/FSets/FSetToFiniteSet.v +++ b/theories/FSets/FSetToFiniteSet.v @@ -107,8 +107,8 @@ Module S_to_Finite_set (U:UsualOrderedType)(M:S with Module E := U). unfold Same_set, Included, mkEns, In. split; intro; set_iff; inversion 1; unfold E.eq in *; auto with sets. split; auto. - swap H1. - inversion H2; auto. + contradict H1. + inversion H1; auto. Qed. Lemma mkEns_Finite : forall s, Finite _ (!!s). |