The Coq mailing list

[Julien Narboux <jnarboux AT narboux.fr>]

Thanks a lot it is almost what I need. 

I changed the indentation style. My version is available here:

https://github.com/jnarboux/corn/blob/master/tools/coqindenter

Julien

2014-06-18 16:28 GMT+02:00 Eelis van der Weegen <eelis AT eelis.net>:

Webpage should be up again now. The script has probably bit-rotted a lot though.

On 2014-06-18 14:50, Bas Spitters wrote:

Eelis once worte:
http://www.eelis.net/coqindent/
It seems to be currently offline, but it is still on github:
https://github.com/c-corn/corn/blob/master/tools/coqindenter

On Tue, Jun 17, 2014 at 4:11 PM, Julien Narboux <jnarboux AT narboux.fr> wrote:

Hi,

Does anyone have a script to automatically indent a Coq *proof* ?
I would like to add curly brackets {} and bullets to an existing proof to
group the tactics solving the same goal.

Cheers,

Julien Narboux