The Coq mailing list

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

Yes, we could do that, at the cost of having to explain that sometimes { 
really means {{…  :-|

    - B


On Mar 8, 2013, at 3:50 PM, Adam Chlipala 
<adamc AT csail.mit.edu>
 wrote:

> On 03/08/2013 03:23 PM, Benjamin C. Pierce wrote:
>> I do want to stay with ascii, to avoid forcing too many people to struggle 
>> with how to edit unicode.  But the other solutions do seem pretty 
>> reasonable -- my current favorite is [{P} c {Q}].  Another option we're 
>> considering is to keep {{P}}c{{q}} but fix up the HTML output so that the 
>> braces come out close together.
> 
> Can you use coqdoc's "printing" command to render "{{" as "{" in HTML, etc.?