Imported Upstream version 8.3.pl2upstream/8.3.pl2

1 files changed, 3 insertions, 3 deletions

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.