coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Generating Proof Trees in CoQ

From: CoqUser CoqUser <coquser AT yahoo.com>
To: Jean-Marc Notin <notin AT lix.polytechnique.fr>, coq-club AT pauillac.inria.fr
Cc: Cedric Auger <Cedric.Auger AT lri.fr>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Generating Proof Trees in CoQ
Date: Mon, 20 Jul 2009 03:49:24 -0700 (PDT)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Message-ID:X-YMail-OSG:Received:X-Mailer:References:Date:From:Subject:To:Cc:In-Reply-To:MIME-Version:Content-Type; b=a8Ck9QMYCvtyMJh+s+lbwFyuto03pPGCQ3oDlKJVyqejD8AbmRRU6VLfmf3BvapWZbkl/IFWb4Qr0jBEejnhIiuzMp8p3MrcWs3lTjjHLOZsXJO9NJBhYqgWMJfcVEZZAX2E+Dae67tc1TM2vjSl43mZ6EKXODUDwXnCeiGm/q4=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I need standard proofs trees as on page 123 of the Coq 8.2 Reference Manual preferably in latex form not dependency graphs.

From: Jean-Marc Notin <notin AT lix.polytechnique.fr>
To: CoqUser CoqUser <coquser AT yahoo.com>
Cc: Cedric Auger <Cedric.Auger AT lri.fr>; coq-club AT pauillac.inria.fr
Sent: Monday, July 20, 2009 10:39:18 AM
Subject: Re: [Coq-Club] Generating Proof Trees in CoQ

CoqUser CoqUser a �crit :
> I don't see any documentation there that answers the question.
> Has anyone ever generated proof trees in CoQ? Is it a feature?
>
There is an external tool to generate dependency graphs from Coq source files: http://www-sop.inria.fr/lemme/coq-graphs/

-- Jean-Marc Notin
CNRS - LIX

[Coq-Club] Generating Proof Trees in CoQ, CoqUser CoqUser
- Message not available
  - Re: [Coq-Club] Generating Proof Trees in CoQ, CoqUser CoqUser
    - Re: [Coq-Club] Generating Proof Trees in CoQ, Jean-Marc Notin
      - Re: [Coq-Club] Generating Proof Trees in CoQ, CoqUser CoqUser
        
        Re: [Coq-Club] Generating Proof Trees in CoQ, Adam Koprowski
        
        Re: [Coq-Club] Generating Proof Trees in CoQ, CHA Reeseo
        
        Re: [Coq-Club] Generating Proof Trees in CoQ, CoqUser CoqUser
        
        Re: [Coq-Club] Generating Proof Trees in CoQ, CoqUser CoqUser
        
        Message not available
        
        Re: [Coq-Club] Generating Proof Trees in CoQ, Anne Pacalet
        
        Re: [Coq-Club] Generating Proof Trees in CoQ, Jean-Francois Monin
- Re: [Coq-Club] Generating Proof Trees in CoQ, Cedric Auger