From 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Tue, 19 Apr 2011 16:44:20 +0200 Subject: Imported Upstream version 8.3.pl2 --- theories/MSets/MSetAVL.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/MSets/MSetAVL.v') 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. -- cgit v1.2.3