Is there a full documentation of Coq's grammar?

Looking for the grammar at the doc requires too much time. Is there a nice page or pdf that full grammar of coq is listed?

The closest thing is in the files fullGrammar and orderedGrammar in the source code. The first shows the grammar without the actions and minimal changes compared to the .mlg files. The second shows a grammar that has been edited for readability. These are big files, over a thousand lines each. But neither is intended to be read by end users.

We’re in the midst of updating the grammar in the doc, which was very much out of date. Look at the Terms section of the Gallina chapter to see what the updated doc looks like. I think the hyperlinks of nonterminals make that easier to read.

The updates to the Terms section that I mentioned don’t appear in the HTML doc linked from the website. You would need the next release or to build from the source code to see them.

The updates Jim is talking about appear in the “development” version of the reference manual, which is continuously deployed at

But more importantly the question is: why do you need to see the full Coq grammar? If this is to write your own parser of Coq’s grammar, that’s something that is very much advised against. I could write more about why it is so and what are the alternative ways of parsing a Coq document if you want.

It should also be mentioned that the Coq grammar is extensible, some more information about this here.

I was just hoping if I could get better understandings in coq with the grammar, but I would like to try what others don’t try at all. Why do you not recommend it, and what are the alternative ways?