The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  I on the other hand would be quite interested in dependency graphs but the links at: http://www-sop.inria.fr/lemme/coq-graphs/ do not work. Any ideas?
   Cheers,

   Adam

On Mon, Jul 20, 2009 at 12:49, CoqUser CoqUser <coquser AT yahoo.com> wrote:

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

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================