diff options
| author | Jim Fehrle | 2019-12-18 23:23:34 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2019-12-28 12:34:47 -0800 |
| commit | 7b143ed46ab2b1b804b834b59533bef5960be9bc (patch) | |
| tree | 97736e1de02a980f21880f4466009707e71821f8 /doc/tools/docgram/productionlist.edit_mlg | |
| parent | bdb5150669d5ac972d3d2b3c9cc2045e77dc9ad5 (diff) | |
Convert productionlists to prodns
Diffstat (limited to 'doc/tools/docgram/productionlist.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/productionlist.edit_mlg | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/doc/tools/docgram/productionlist.edit_mlg b/doc/tools/docgram/productionlist.edit_mlg index 42d94e76bb..8170b71e7a 100644 --- a/doc/tools/docgram/productionlist.edit_mlg +++ b/doc/tools/docgram/productionlist.edit_mlg @@ -13,32 +13,6 @@ DOC_GRAMMAR -EXPAND: [ | ] - -RENAME: [ -| name_alt names_tuple -| binder_list binders -| binder_list_opt binders_opt -| typeclass_constraint_list_comma typeclass_constraints_comma -| universe_expr_list_comma universe_exprs_comma -| universe_level_list_opt universe_levels_opt -| name_list names -| name_list_comma names_comma -| case_item_list_comma case_items_comma -| eqn_list_or_opt eqns_or_opt -| eqn_list_or eqns_or -| pattern_list_or patterns_or -| fix_body_list fix_bodies -| arg_list args -| arg_list_opt args_opt -| evar_binding_list_semi evar_bindings_semi -] - -binders_opt: [ -| REPLACE binders_opt binder -| WITH binders -] - (* this is here because they're inside _opt generated by EXPAND *) SPLICE: [ | ltac_info |