diff options
Diffstat (limited to 'doc/tools/docgram/prodn.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/prodn.edit_mlg | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/tools/docgram/prodn.edit_mlg b/doc/tools/docgram/prodn.edit_mlg index a28d07636a..37197a1fec 100644 --- a/doc/tools/docgram/prodn.edit_mlg +++ b/doc/tools/docgram/prodn.edit_mlg @@ -12,3 +12,13 @@ (* Contents used to generate prodn in doc *) DOC_GRAMMAR + +(* todo: doesn't work, gives +ltac_match: @match_key @ltac_expr with {? %| } {+| @ltac_expr } end +instead of +ltac_match: @match_key @ltac_expr with {? %| } {+| {| @match_pattern | _ } => @ltac_expr } end + +SPLICE: [ +| match_rule +] +*) |