summaryrefslogtreecommitdiff
path: root/theories/FSets
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:44:20 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:44:20 +0200
commit9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (patch)
treea418d1edb3d53cdb4185b9719b7a70822cf5a24d /theories/FSets
parent6b691bbd2101fd39395c0d2135fd7c06a8915e14 (diff)
Imported Upstream version 8.3.pl2upstream/8.3.pl2
Diffstat (limited to 'theories/FSets')
-rw-r--r--theories/FSets/FMapAVL.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index cf0449f8..49f595d7 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -8,7 +8,7 @@
(* Finite map library. *)
-(* $Id: FMapAVL.v 13427 2010-09-17 17:37:52Z letouzey $ *)
+(* $Id: FMapAVL.v 13768 2011-01-06 13:55:35Z glondu $ *)
(** * FMapAVL *)
@@ -78,9 +78,9 @@ Definition empty := Leaf.
Definition is_empty m := match m with Leaf => true | _ => false end.
-(** * Appartness *)
+(** * Membership *)
-(** The [mem] function is deciding appartness. It exploits the [bst] property
+(** The [mem] function is deciding membership. It exploits the [bst] property
to achieve logarithmic complexity. *)
Fixpoint mem x m : bool :=
@@ -705,7 +705,7 @@ Proof.
destruct m; simpl; intros; try discriminate; red; intuition_in.
Qed.
-(** * Appartness *)
+(** * Membership *)
Lemma mem_1 : forall m x, bst m -> In x m -> mem x m = true.
Proof.