The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/20/2014 11:10 AM, Pierre Courtieu wrote:
> 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.

Beware that sometimes PG's indenter (even the most recent dev version, 
which I use) makes some unusual choices, probably due to trying to cope 
with the new bullets syntax.  For instance:

  intros.
tac.

gets re-indented as follows, but only when certain bullet-esque intro 
patterns are used:

  intros x **.
         tac.

[In case e-mail formatting throws that off - the tac on the second line 
is lined up under x.]

-- Jonathan