The Coq mailing list

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

Yes it does. This was implemented at about the same time bullets were
introduced in coq (actually it was implemented *before* to convince
dev team that bullets were a good idea :)).

I am not sure a release of pg was done since that however. Try dev
version of pg.

Beware that you need to follow the precedence - > +> * to make
indentation work. Nesting bullets inside { } is supported.

It is a bit fragile (sometimes very slow, sometimes (rarely) buggy)
but it works. It is not very customizable currently.

P.

2014-06-20 9:27 GMT+02:00 Julien Narboux 
<jnarboux AT narboux.fr>:
> Hi Pierre,
>
> Is ProofGeneral indenting proofs ? the version I tried before posting this
> message was indenting only Lemma/Sections...
>
> Cheers,
>
> Julien
>
>
> 2014-06-20 1:38 GMT+02:00 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
>> >>
>> >>
>> >
>
>