aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/prodn.edit_mlg
AgeCommit message (Expand)Author
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
2019-07-19Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg filesJim Fehrle