The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

Note that proofgeneral has indentation working, use tab for a single
line and M-x indent-region for indenting a whole region (it may be
slow for big files with big modules of sections). bug reports welcome.

Best,
Pierre


2014-06-19 16:31 GMT+02:00 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
>>
>>
>