coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Generating Proof Trees in CoQ

From: CoqUser CoqUser <coquser AT yahoo.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Generating Proof Trees in CoQ
Date: Mon, 20 Jul 2009 00:49:44 -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:Date:From:Subject:To:MIME-Version:Content-Type; b=SJifO8AommE4AjiPaB1beaO+bG6jWtK++anJqWhRUPs7zfXgBLY5QwMgmOD7rMkk6Sqkcicm9bdpv5vF0QXWpaE/6U9N1cagmtyotdTIi6MCmXL/abGcIb2Zzbr10zNFc0dhvfx6aUJ5lHlq9ai1Hy++xfGCwjkM16umJM+n708=;
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Is it possible to generate proof trees formatted like page 123 of Coq v.8.2 Reference Manual directly from Coq proof text files? The reference manual mentions coq-tex, but there's no documentation.

[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