coq/doc/tools/docgram/prodn.edit_mlg, branch master The formal proof system Doc_grammar: Update cmd:: and tacn:: constructs in .rsts 2020-03-25T22:05:44+00:00 Jim Fehrle 2020-03-25T17:21:32+00:00 245af3e197c36482931248479c8eca5d0e6459a6 Remove unneeded source and output files Move all commands under command NT Add a lot of edits for commands and tactics 
Remove unneeded source and output files
Move all commands under command NT
Add a lot of edits for commands and tactics
Update headers in the whole code base. 2020-03-18T11:15:43+00:00 Théo Zimmermann 2020-03-18T11:14:26+00:00 a99776e10e0b2198d2b811ad82631111fb450f8a Add headers to a few files which were missing them. 
Add headers to a few files which were missing them.
Update grammar in the Terms section of Gallina chapter 2019-11-20T16:53:00+00:00 Jim Fehrle 2019-08-05T22:10:32+00:00 b4eca882b6692b6374dfff8517f9f5a5cc4970f5 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. 
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.
Introduce doc_gram, a utilty for extracting Coq's grammar from .mlg files 2019-07-19T16:50:31+00:00 Jim Fehrle 2019-01-09T23:32:52+00:00 cf868740c3d18ee9ce9a6b38dd617784625a3cae and inserting it into the .rst files 
and inserting it into the .rst files