diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-07 21:20:00 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-07 21:20:00 +0000 |
| commit | e6e65421f9b3de20d294b8e6be74806359471a7c (patch) | |
| tree | 55298d7f3a9d6da628931dfe1b1236be6ccecc77 /theories/FSets/FSetProperties.v | |
| parent | ec850ff623801e514b3ed0a42beb6f7984992520 (diff) | |
repair FSets/FMap after the change in setoid rewrite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10636 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/FSets/FSetProperties.v')
| -rw-r--r-- | theories/FSets/FSetProperties.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index f3da02a83..1ea669eb8 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -859,8 +859,8 @@ Module OrdProperties (M:S). apply (@filter_sort _ E.eq); auto with set; eauto with set. constructor; auto. apply (@filter_sort _ E.eq); auto with set; eauto with set. - rewrite ME.Inf_alt; auto; intros. - apply (@filter_sort _ E.eq); auto with set; eauto with set. + rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with set). + intros. rewrite filter_InA in H1; auto; destruct H1. rewrite leb_1 in H2. rewrite <- elements_iff in H1. |