coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] coqdoc and documenting constructors of inductives/fields of records.

From: Adam Koprowski <adam.koprowski AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] coqdoc and documenting constructors of inductives/fields of records.
Date: Thu, 25 Feb 2010 18:05:19 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type; b=VIDnauKEiaBAgLYJJHyAYyuoOYmyjrA4y8mzMB2LABcA6K698VJtx1QR2+6pDnymC0 B/TF4Dsl5/plpoGhQ2QJIIM2Pazxxz9/Pul6ctiGop9NJRkyscKwt6jUFDr0YvnBNF3S 4WmMOgvW6S4Gb9uN9UWdmgYoO9++jYoljHbR0=

�� Dear all,

��Is there a way to document constructors of (big) inductive types and/or fields of record types with coqdoc? I think I once saw a development achieving that with (**r ... *) annotations, but I cannot find it in the documentation and neither does it seem to work for me.�

��Best,

��Adam

--
Adam Koprowski � [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate � �[http://mlstate.com, 15 rue Berlier, 75013 Paris, France]

[Coq-Club] coqdoc and documenting constructors of inductives/fields of records., Adam Koprowski