The Coq mailing list

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

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.