coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] finite sets in proofs

From: Chantal Keller <chantal.keller AT wanadoo.fr>
To: St�phane Lescuyer <stephane.lescuyer AT inria.fr>, Thomas Braibant <thomas.braibant AT gmail.com>
Cc: Christian Doczkal <doczkal AT ps.uni-sb.de>, coq-club AT inria.fr
Subject: Re: [Coq-Club] finite sets in proofs
Date: Fri, 26 Mar 2010 15:56:05 +0100

Thanks to both of you. I indeed probably deduce wrong conclusions when I
tried FSets, from a call to Eval vm_compute.

Sorry for this erroneous e-mail.

Chantal.

[Coq-Club] finite sets in proofs, Christian Doczkal
- Re: [Coq-Club] finite sets in proofs, Pierre Casteran
- Re: [Coq-Club] finite sets in proofs, AUGER
- RE: [Coq-Club] finite sets in proofs, Georges Gonthier
- Re: [Coq-Club] finite sets in proofs, Chantal Keller
  - Re: [Coq-Club] finite sets in proofs, Thomas Braibant
    - Re: [Coq-Club] finite sets in proofs, Chantal Keller
      - Re: [Coq-Club] finite sets in proofs, Thomas Braibant
      - Re: [Coq-Club] finite sets in proofs, St�phane Lescuyer
        
        Re: [Coq-Club] finite sets in proofs, Pierre Letouzey
        
        Re: [Coq-Club] finite sets in proofs, Chantal Keller
      - [Coq-Club] Yet another dependent type question, Pierre-Marie P�drot
        
        Re: [Coq-Club] Yet another dependent type question, Adam Chlipala
        
        Re: [Coq-Club] Yet another dependent type question, Pierre Corbineau
        
        Re: [Coq-Club] Yet another dependent type question, Pierre-Marie P�drot
        Re: [Coq-Club] Yet another dependent type question, Michael Shulman
        Re: [Coq-Club] Yet another dependent type question, Hugo Herbelin
        Re: [Coq-Club] Yet another dependent type question, Michael Shulman
        Re: [Coq-Club] Yet another dependent type question, Hugo Herbelin