coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof tree visualization

From: Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>
To: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
Cc: "Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>, coq-club AT inria.fr
Subject: Re: [Coq-Club] proof tree visualization
Date: Sun, 1 May 2011 00:22:55 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; b=VMzUYACYGb2Ww3kDSctFdUpF8nwuv6dtMv7jK7X7gH3Bm57WsNr+N5XZP2fQecllMH TF1rW3ONsMVgEYEJYA4gSww2R9CF3CW9N5q47VxFSoZDdbCQp4vXSWwGvrR/ZP3oOPaV FbzYSQTJSsCUsuxNMVQoEiPwR/qgZt9wOrSj4=

Hi Arnaud
2011/4/29 Arnaud Spiwack
<aspiwack AT lix.polytechnique.fr>:
> It is quite likely that such features make their way to Coq. Though not for
> the next release I'm afraid.

Do you have any details on that? What sort of plans? I'm not talking
about a time line, just to have an idea of what kind of feature we can
expect. Are you talking about the bullets, or something more advanced?

I would really love to have more informations!

Alexandre

Re: [Coq-Club] proof tree visualization, Alexandre Pilkiewicz
- Re: [Coq-Club] proof tree visualization, Arnaud Spiwack
  - Re: [Coq-Club] proof tree visualization, Alexandre Pilkiewicz