diff options
Diffstat (limited to 'doc/tools/docgram/common.edit_mlg')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 853b818498..5bf122078d 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -387,7 +387,7 @@ gallina: [ | REPLACE thm_token ident_decl binders ":" lconstr LIST0 [ "with" ident_decl binders ":" lconstr ] | WITH thm_token ident_decl binders ":" type LIST0 [ "with" ident_decl binders ":" type ] | DELETE assumptions_token inline assum_list -| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| REPLACE finite_token LIST1 inductive_definition SEP "with" | WITH "Inductive" inductive_definition LIST0 ( "with" inductive_definition ) | "CoInductive" inductive_definition LIST0 ( "with" inductive_definition ) | "Variant" inductive_definition LIST0 ( "with" inductive_definition ) @@ -405,11 +405,6 @@ gallina: [ | WITH "Scheme" scheme LIST0 ( "with" scheme ) ] -DELETE: [ -| private_token -| cumulativity_token -] - constructor_list_or_record_decl: [ | OPTINREF ] @@ -737,12 +732,8 @@ assumption_token: [ | WITH [ "Variable" | "Variables" ] ] -legacy_attrs: [ -| OPT [ "Local" | "Global" ] OPT [ "Polymorphic" | "Monomorphic" ] OPT "Program" OPT [ "Cumulative" | "NonCumulative" ] OPT "Private" -] - all_attrs: [ -| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) OPT legacy_attrs +| LIST0 ( "#[" LIST0 attribute SEP "," "]" ) LIST0 legacy_attr ] vernacular: [ |