diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-14 10:30:56 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-14 10:30:56 +0000 |
| commit | ded45010b86ccc2203262f13340495b200f742bd (patch) | |
| tree | 66da07d51dfb5432f78055737a25ec081545e82e /theories/FSets | |
| parent | 84c6dc6677ddf527a51eed62adcf8ad5daa77ca1 (diff) | |
Simplify eauto and fix it for compatibility, allowing full delta during
unification for exact hints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12239 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets')
| -rw-r--r-- | theories/FSets/FMapFacts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index cd80003a2..e116067af 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -790,7 +790,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). intros. symmetry. unfold eqb. rewrite <- findA_NoDupA, InA_rev, findA_NoDupA - by eauto using NoDupA_rev; eauto. apply H0. + by eauto using NoDupA_rev; eauto. case_eq (findA (eqb k) (rev l)); auto. intros e. unfold eqb. |