aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/fullGrammar
AgeCommit message (Collapse)Author
2020-04-13Update syntax of Import / Export in documentation.Théo Zimmermann
2020-04-07Support universe bindings and universe constraints in Let definitions.Théo Zimmermann
Let vs Definition / Example syntax was split in 7c28130 for parsing reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could be introduced. This split is probably the reason why Let was overlooked when support for universe bindings and universe constraints were added to Definition and variants.
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-19Update fullGrammar, common.edit_mlg and orderedGrammar...Théo Zimmermann
following changes to attribute parsing.
2020-03-19Update fullGrammar and common.edit_mlg following #11839.Théo Zimmermann
2020-03-09Remove some productionlistsJim Fehrle
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
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-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-08-14 16:01:23 +0000