coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] MSetFullAVL location

From: Thomas Braibant <thomas.braibant AT gmail.com>
To: Jim Apple <coq-club AT jbapple.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] MSetFullAVL location
Date: Mon, 13 Sep 2010 13:36:48 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=WkywhVTEKoF0ysEVuNJhmHjWl1a0niY9pWr58CHhHLHmR4Yiut+aR58DA5yRjEeL1Q p+IdaWU3Mm1KYhDqACGepBgYaKvDJJaKDetAAtEYIyNh0asuHXI+SzShuCx67zoQ0IP2 26L+F3e4TIi/T7RcvgUrWC46FWLQYMsdu8Nzo=

Indeed, the file FSetFullAVL used to exist in 8.2, but I cannot find
it either in the trunk nor in the upcoming 8.3 (the MSetFullAVL
version that is claimed to exist is not there, nor is the former
FSetFullAVL version).

Maybe it is just a glitch with the version control the devs use for Coq.

thomas

On Sun, Sep 12, 2010 at 4:24 PM, Jim Apple
<coq-club AT jbapple.com>
wrote:
> In the 8.3rc1 sources, MSetAVL.v refers the reader MSetFullAVL for
> proofs of the balance conditions and for non-structually-recursive
> functions for a few operations, but MSetFullAVL.v is not in
> theories/MSets.
>
> Doe anyone know where I might find MSetFullAVL.v? I did find
> FMapFullAVL.v in theories/FSets.
>
> Jim
>

[Coq-Club] MSetFullAVL location, Jim Apple
- Re: [Coq-Club] MSetFullAVL location, Thomas Braibant
- Re: [Coq-Club] MSetFullAVL location, Pierre Letouzey