The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Since this thread in in the outside-the-box-thinking category, people
may be interested by Elastic Tabstops that solve this indentation
problem:
  http://nickgravgaard.com/elastic-tabstops/

On Fri, Mar 11, 2016 at 10:22 AM, Pierre Courtieu
<pierre.courtieu AT gmail.com>
 wrote:
> Hi,
>
> Concerning prettification there is one problem that is difficult to solve:
> indentation. Look for example at the following code that is indented for
> non-prettified display:
>
> forall x y, x +
>             y.
>
> This will not look good if prettified:
>
> ∀ x y, x +
>             y.
>
> And conversely a good indentation in prettified mode would not look good in
> non prettified.
>
> In pg+company-coq indentation is done according to the current mode
> (prettified or not), but user opening the file with the other mode will have
> ugly indentation.
>
> P.