summaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/FSets/FMapAVL.v8
-rw-r--r--theories/MSets/MSetAVL.v6
2 files changed, 7 insertions, 7 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.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index c41df7c2..96580749 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -82,9 +82,9 @@ Definition empty := Leaf.
Definition is_empty s :=
match s with Leaf => true | _ => false end.
-(** ** Appartness *)
+(** ** Membership *)
-(** The [mem] function is deciding appartness. It exploits the
+(** The [mem] function is deciding membership. It exploits the
binary search tree invariant to achieve logarithmic complexity. *)
Fixpoint mem x s :=
@@ -792,7 +792,7 @@ Proof.
split; auto. try discriminate. intro H; elim (H x); auto.
Qed.
-(** * Appartness *)
+(** * Membership *)
Lemma mem_spec : forall s x `{Ok s}, mem x s = true <-> InT x s.
Proof.