The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Well, I cannot be very specific but I was thinking of

1/ Building on bullets (currently experimental) for robust proofs. There is also (already in trunk) BeginSubproof and EndSuproof keywords (the names may change) which have similar effect. Other keywords/semantics can be readily implemented if there is some support for it.
2/ Facilities for naming goals. I haven't thought much of a final form for this.
3/ Extra beefy destruction tactics, with syntax such as: Destruct n. Case S 0. […] Case 0. […] Case S (S p). […]

None of these are promises. Rather things I'm willing to spend some time thinking of at some point.


Arnaud

On 1 May 2011 00:22, Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org> wrote:

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