The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Bas Spitters wrote:
> Is there a pretty printer for coq sources?
> I would be especially interested in having a tool for indentation.
>
>
> n-1 leading spaces for n open goals. This makes proof scripts easier 
> to maintain.

If your proof scripts are deeply nested enough for you to want to use 
indentation to indicate nesting depth, then you should probably be 
breaking your proofs into more lemmas that you add as proof hints. ;)

I purposely don't believe that proof scripts with non-trivial nesting 
can ever be easy to maintain, regardless of how you display them.  I 
recommend using automation to prove every theorem with a single tactic.  
There are examples of this kind of proof in two projects that I've 
worked on recently:
   http://ltamer.sourceforge.net/
   http://ynot.cs.harvard.edu/
...and I try to explain how to do it in this book-in-progress:
   http://adam.chlipala.net/cpdt/