aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/FSets/FSetProperties.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/FSets/FSetProperties.v')
-rw-r--r--theories/FSets/FSetProperties.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index 2315dc532..f6eebdc17 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -546,7 +546,7 @@ Module Properties (M: S).
rewrite leb_1 in H2.
rewrite <- elements_iff in H1.
assert (~E.eq x y).
- swap H; rewrite H3; auto.
+ contradict H; rewrite H; auto.
ME.order.
intros.
rewrite filter_InA in H1; auto; destruct H1.