aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/README.md
AgeCommit message (Expand)Author
2020-06-08Add MOVEALLBUT operationJim Fehrle
2020-03-29Add -no-update command line option to doc_grammar for DuneJim Fehrle
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
2020-03-12Dune build rules for doc_grammar and fullGrammar.Théo Zimmermann
2020-02-24Add OPTREF and INSERTALL editing operationsJim Fehrle
2019-12-28Convert productionlists to prodnsJim Fehrle
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