1 files changed, 32 insertions, 5 deletions
diff --git a/doc/tools/docgram/README.md b/doc/tools/docgram/README.md
index 2d29743d78..14f87e5885 100644
--- a/doc/tools/docgram/README.md
+++ b/doc/tools/docgram/README.md
@@ -37,13 +37,16 @@ for documentation purposes:
 1.  The tool reads all the `mlg` files and generates `fullGrammar`, which includes
     all the grammar without the actions for each production or the OCaml code.  This
     file is provided as a convenience to make it easier to examine the (mostly)
-    unprocessed grammar of the mlg files with less clutter.  Nonterminals that use
-    levels (`"5" RIGHTA` below) are modified, for example:
+    unprocessed grammar of the mlg files with less clutter.  This step includes two
+    transformations that rename some nonterminal symbols:
+
+    First, nonterminals that use levels (`"5" RIGHTA` below) are modified, for example:
 
     ```
     tactic_expr:
       [ "5" RIGHTA
         [ te = binder_tactic -> { te } ]
+      [ "4"   ...
     ```
 
     becomes
@@ -55,6 +58,17 @@ for documentation purposes:
     ]
     ```
 
+    Second, nonterminals that are local to an .mlg will be renamed, if necessary, to
+    make them unique.  For example, `strategy_level` is defined as a local nonterminal
+    in both `g_prim.mlg` and in `extraargs.mlg`.  The nonterminal defined in the former
+    remains `strategy_level` because it happens to be processed before the latter,
+    in which the nonterminal is renamed to `EXTRAARGS_strategy_level` to make the local
+    symbol unique.
+
+    Nonterminals listed after `GLOBAL:` are global; otherwise they are local.
+
+    References to renamed symbols are updated with the modified names.
+
 2.  The tool applies grammar editing operations specified by `common.edit_mlg` to
     generate `editedGrammar`.
 
@@ -227,9 +241,22 @@ to the grammar.
 
 The end of the existing `prodn` is recognized by a blank line.
 
-### Other details
+### Tagging productions
+
+`doc_grammar` tags the origin of productions from plugins that aren't automatically
+loaded.  In grammar files, they appear as `(* XXX plugin *)`.  In rsts, productions
+generated by `.. insertprodn` will include where relevant three spaces as (a delimiter)
+and a tag name after each production, which Sphinx will show on the far right-hand side
+of the production.
+
+The origin of a production can be specified explicitly in `common.edit_mlg` with the
+`TAG name` appearing at the end of a production.  `name` must be in quotes if it
+contains whitespace characters.  Some edit operations preserve the
+tags, but others, such as `REPLACE ... WITH ...` do not.
+
+A mapping from filenames to tags (e.g. "g_ltac2.mlg" is "Ltac2") is hard-coded as is
+filtering to avoid showing tags for, say, Ltac2 productions from appearing on every
+production in that chapter.
 
-The output identifies productions from plugins that aren't automatically loaded with
-`(* XXX plugin *)` in grammar files and with `(XXX plugin)` in productionlists.
 If desired, this mechanism could be extended to tag certain productions as deprecated,
 perhaps in conjunction with a coqpp change.