diff options
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 5b19b7fc55..cd96693bf0 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -553,7 +553,6 @@ term_cast: [ | term10 ":" type | term10 "<:" type | term10 "<<:" type -| term10 ":>" ] term_match: [ @@ -1096,7 +1095,7 @@ command: [ | "Undelimit" "Scope" scope_name | "Bind" "Scope" scope_name "with" LIST1 class | "Infix" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] -| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" ) +| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) | "Notation" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ] | "Format" "Notation" string string string | "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) @@ -1540,7 +1539,7 @@ class: [ syntax_modifier: [ | "at" "level" natural | "in" "custom" ident OPT ( "at" "level" natural ) -| LIST1 ident SEP "," "at" level +| LIST1 ident SEP "," [ "at" level | "in" "scope" ident ] | ident "at" level OPT binder_interp | ident explicit_subentry | ident binder_interp @@ -1856,7 +1855,6 @@ simple_tactic: [ | "zify_iter_let" ltac_expr (* micromega plugin *) | "zify_elim_let" (* micromega plugin *) | "nsatz_compute" one_term (* nsatz plugin *) -| "omega" (* omega plugin *) | "protect_fv" string OPT ( "in" ident ) | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) | "field_lookup" ltac_expr "[" LIST0 one_term "]" LIST1 one_term (* ring plugin *) |