The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Clément,

> I think prettification offers an interesting middle ground (see an example 
> at
> https://github.com/cpitclaudel/company-coq/#prettification-of-operators-
> types-and-subscripts; these two screenshots show the same Emacs buffer,
> with and without the prettification layer). This should allow both kinds of 
> SW
> engineers to work on the same files.

Yes indeed. Looking into the fact that some people for whatever reason don't 
like fancy notations, it is likely the best option to keep the files in ASCII 
and just display and edit them on the fly in fancy notation.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928