The Coq mailing list

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

In the Software Foundations text, we are currently using the notation

   {{P}} c {{Q}}

for Hoare triples, which is not completely awful but rather heavy.  Is it 
hopeless to dream that we might somehow be able to get Coq's Notation 
mechanism to accept the standard notation

   {P} c {Q}

or something similar?

Thanks

    - Benjamin