diff options
| author | Jim Fehrle | 2019-08-05 15:10:32 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2019-11-20 08:53:00 -0800 |
| commit | b4eca882b6692b6374dfff8517f9f5a5cc4970f5 (patch) | |
| tree | ed72a4b0a4cc67c4a988349fb28e0600e7f03ea7 /dev/include_dune | |
| parent | 4aa756934eb37c6b6d70eddf2b46871bb8ff0956 (diff) | |
Update grammar in the Terms section of Gallina chapter
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.
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions