The Coq mailing list

[Pierre-Marie Pédrot <pierremarie.pedrot AT ens-lyon.fr>]

AUGER wrote:
> I think this feature should be "consistant with Coq spirit",
> but it is not implemented so.

Yet obviously it deserves to, so I filed a bug report:

http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2291

Feel free to add some details.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature