diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-21 00:03:14 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-21 00:03:14 +0000 |
| commit | 7109daa08ff5be5bf28902d9b060cccf73375b4e (patch) | |
| tree | 7c85db35aaea76d402232d5545a1742a9088dbeb /theories/FSets/FSetFacts.v | |
| parent | 97b74d43fe5f6070992c4824f823a9725620944e (diff) | |
Cleanup attempt of Hints in *Interface.v files.
See recent discussion in coq-club.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10243 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FSetFacts.v')
| -rw-r--r-- | theories/FSets/FSetFacts.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index ac0227f5c..e83b861fb 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -258,7 +258,8 @@ apply H0; auto. symmetry. rewrite H0; intros. destruct H1 as (_,H1). -apply H1; auto. +apply H1; auto with set. +apply elements_2; auto with set. Qed. Lemma exists_b : compat_bool E.eq f -> @@ -271,7 +272,7 @@ destruct (existsb f (elements s)); destruct (exists_ f s); auto; intros. rewrite <- H1; intros. destruct H0 as (H0,_). destruct H0 as (a,(Ha1,Ha2)); auto. -exists a; auto. +exists a; intuition; auto with set. symmetry. rewrite H0. destruct H1 as (_,H1). @@ -420,7 +421,7 @@ Add Relation t Subset Add Morphism In with signature E.eq ==> Subset ++> impl as In_s_m. Proof. -unfold Subset, impl; intros; eauto. +unfold Subset, impl; intros; eauto with set. Qed. Add Morphism Empty with signature Subset --> impl as Empty_s_m. |