The Coq mailing list

["Benjamin C. Pierce" <bcpierce AT cis.upenn.edu>]

> Obviously this is not a very important issue.

Not in itself, but it's an aspect of an issue that's becoming more important 
over time: in general, Coq's notations are not nearly as nice to look at as, 
say, Isabelle's.  Doesn't matter so much in day to day theorem proving work, 
but it becomes more of a problem when Coq proofs get shown to students or 
used in publications.  

I don't have a specific proposal to make here, but clearly it would be a good 
start if unicode worked as smoothly as possible.  My own experiments with it 
have been unsatisfying: the basic functionality seems OK, but I find the 
unicode fonts that emacs/PG give me for .v files by default to be really 
hideous, and in a couple of hours of playing around I wasn't able to do much 
better (and I was worried that others would not be able to replicate my 
"look" if I did find a combination that worked well).

    - Benjamin