coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>
To: CoqUser CoqUser <coquser AT yahoo.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Generating Proof Trees in CoQ
Date: Mon, 20 Jul 2009 16:16:21 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Mailscanner-null-check: 1248704402.15136@9cw1uciBCo/c63TAYw+OHA

Dear Coq user,

Just a non-technical point.
Please that almost all of us on this list are Coq users as well,
By some kind of netiquette, we sign with our names and preferably
present ourselves the first time.

Regards,
  JF

On Mon, Jul 20, 2009 at 03:49:24AM -0700, CoqUser CoqUser wrote:
> I need standard proofs trees as on page 123 of the Coq 8.2 Reference Manual
> preferably in latex form not dependency graphs.

--
Jean-Francois Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     mob (+33 | 0) 6 81 23 30 05
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46

[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