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/FMapFacts.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/FMapFacts.v')
| -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 78962fd1b..993f1ae79 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1214,7 +1214,6 @@ Module OrdProperties (M:S). constructor; auto with map. apply (@filter_sort _ eqke); auto with map; clean_eauto. rewrite (@InfA_alt _ eqke); auto with map; try (clean_eauto; fail). - apply (@filter_sort _ eqke); auto with map; clean_eauto. intros. rewrite filter_InA in H1; auto with map; destruct H1. rewrite leb_1 in H2. @@ -1224,6 +1223,7 @@ Module OrdProperties (M:S). contradict H. exists e0; apply MapsTo_1 with t0; auto. ME.order. + apply (@filter_sort _ eqke); auto with map; clean_eauto. intros. rewrite filter_InA in H1; auto with map; destruct H1. rewrite gtb_1 in H3. |