aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/README.md
AgeCommit message (Expand)Author
2020-11-23Add COPYALL and APPENDALL edit ops, drop unneeded codeJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-09-11Remove outdated references to productionlist.Théo Zimmermann
2020-07-08Add tags in prodn indicating productions that are from plugins,Jim Fehrle
2020-07-08Make local nonterminal definitions unique when necessaryJim Fehrle
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:02:44 +0000