The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

  I'm currently (past few days, trying to) writing a parser for Coq. With the exception of Notation (for which I hard coded the common cases I use) and proper handling of precedence (i.e. "1 + 2 * 3" is incorrectly parsed as "(1+2)*3"), everything appears to work.

  Courses I had previously take in compilers / automata theory tend to assume that the grammar is fixed before the program is compiled. Notation breaks this assumption. Can someone explain to me (or point me at a paper) on the theoretical foundations behind notation and how it's implemented?

Thanks!