aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/doc_grammar.ml
AgeCommit message (Collapse)Author
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-23Add COPYALL and APPENDALL edit ops, drop unneeded codeJim Fehrle
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-09Add additional escape sequences for notationsJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-11-05Merge numeral and string notation pluginsPierre Roux
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-22Make no match/multiple match for tacn/cmd an errorJim Fehrle
Always generate prodn* files if edits succeed
2020-10-19Better message and avoid an infinite SPLICE loopJim Fehrle
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-07-08Add tags in prodn indicating productions that are from plugins,Jim Fehrle
filtered-only show Ltac2 tags outside of ltac2.rst
2020-07-08Make local nonterminal definitions unique when necessaryJim Fehrle
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-06-08Add NOTINRSTS nonterminal to suppress messagesJim Fehrle
2020-06-08Report an error for empty (sub)productionsJim Fehrle
(Sphinx notations don't support these.)
2020-06-08Add MOVEALLBUT operationJim Fehrle
2020-06-08Refactor SELF code for clarityJim Fehrle
Handle SELF within nested constructs more clearly
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-10Suppress the space after "#" when printing productionsJim Fehrle
to reflect lexer requirement for no space
2020-04-10Ignore subscripts in notation for matching cmds and tacsJim Fehrle
2020-04-10Fix prefix matchingJim Fehrle
2020-03-29Add -no-update command line option to doc_grammar for DuneJim Fehrle
Fix makefile glitches
2020-03-25Doc_grammar: Update cmd:: and tacn:: constructs in .rstsJim Fehrle
Remove unneeded source and output files Move all commands under command NT Add a lot of edits for commands and tactics
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-09Remove some productionlistsJim Fehrle
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-24Add OPTREF and INSERTALL editing operationsJim Fehrle
Show effect of edits to edited nt in PRINT Add cmdv:: info to prodnCommands Supporting code globally replaces a given "substring" in productions with another. (Substring over doc_symbols, not over characters.)
2020-02-24Generate prodnCommands file that compares commands in the grammar toJim Fehrle
those in the rsts.
2019-12-28Convert productionlists to prodnsJim Fehrle
2019-11-20Update grammar in the Terms section of Gallina chapterJim Fehrle
Update doc_grammar tool The grammar in the doc is generated semi-automatically with doc_grammar: - the grammar is automatically extracted from the mlg files - developer-prepared editing scripts *.mlg_edit modify the extracted grammar for clarity, simplicity and ordering of productions - chunks of the resulting grammar are automatically inserted into the rsts using instructions embedded in the rsts Running doc_grammar is currently a manual step. The grammar updates in the rst files have been manually reviewed.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:26:49 +0000