From ba92af4800afd90c03d5f6e277085cd690023415 Mon Sep 17 00:00:00 2001
From: glondu
Date: Thu, 6 Jan 2011 13:53:43 +0000
Subject: s/appartness/membership/g (Closes: #2470)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13767 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/FSets/FMapAVL.v | 6 +++---
 theories/MSets/MSetAVL.v | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index f9dda51255..516015ab96 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -76,9 +76,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 :=
@@ -703,7 +703,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 349cdedf7b..253267fc8d 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -80,9 +80,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 :=
@@ -790,7 +790,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.
-- 
cgit v1.2.3