Thanks Theo. Let’s hope we someone can chip in for the rich lifestyle that Coq’s grammar has. I am very curious about it!
Also, is there a difference between the (evolving) tactic grammar and the (evolving) proof script grammar and (evolving) formula Coq term grammar? Or are they all the same under the (evolving) proof script grammar?
Thanks again!