aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram
AgeCommit message (Collapse)Author
2019-07-28Update documentation on tokens, use "int" and "num"Jim Fehrle
for integers and natural nums
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle
and inserting it into the .rst files