The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

On Jan 3, 2014, at 6:40 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

I'm often running into situations where a definition A depends on some definition B and hence
A cannot be defined(in Coq) before defining B.
However, while communicating the idea to humans via coqdoc, a top down explanation is more suitable, i.e. the definition of B would seem boring/useless until the definition of A is shown to motivate it.

Coqdoc does not seem to provide a way to output definitions and the associated comments in an order that is different that the order in which they appear in the .v file.
Is there an easy way to get around this limitation?

Currently, I have to split the .v file such that the definitions of A and B are in different .v files. Then I include the output .tex files of coqdoc in the
desired order in the main .tex file.

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/

I would suggest that it is a very useful limitation which makes it difficult to hide things from the reader :)

V.