coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

[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