Imported Upstream version 8.3.pl2upstream/8.3.pl2

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.