The Coq mailing list

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

2014-06-20 17:50 GMT+02:00 Jonathan 
<jonikelee AT gmail.com>:
> 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.

Hi, this is exactly the kind of bug that can remain but this one was
fixed in dev release since a long time. I can't reproduce it.

P.