diff options
| author | Pierre Roux | 2020-09-12 09:13:44 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-10-30 14:17:43 +0100 |
| commit | 3a25b967a944fe37e1ad54e54a904d90311ef381 (patch) | |
| tree | cbc2f3325788f61c32d7b678a231741fa5ba0ae8 /doc/tools/docgram/orderedGrammar | |
| parent | 2d44c8246eccba7c1c452cbfbc6751cd222d0a6a (diff) | |
Renaming numnotoption into number_modifier
Diffstat (limited to 'doc/tools/docgram/orderedGrammar')
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 12a7bc684d..a972ad4719 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -884,8 +884,8 @@ command: [ | "Print" "Rings" (* ring plugin *) | "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *) | "Print" "Fields" (* ring plugin *) -| "Number" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier -| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT numeral_modifier +| "Number" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier +| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident ) | "Typeclasses" "Transparent" LIST1 qualid | "Typeclasses" "Opaque" LIST1 qualid @@ -910,6 +910,7 @@ command: [ | "Derive" "Dependent" "Inversion_clear" ident "with" one_term "Sort" sort_family | "Declare" "Left" "Step" one_term | "Declare" "Right" "Step" one_term +| "Numeral" "Notation" qualid qualid qualid ":" scope_name OPT number_modifier | "String" "Notation" qualid qualid qualid ":" scope_name | "SubClass" ident_decl def_body | thm_token ident_decl LIST0 binder ":" type LIST0 [ "with" ident_decl LIST0 binder ":" type ] @@ -1269,7 +1270,7 @@ field_mod: [ | "completeness" one_term (* ring plugin *) ] -numeral_modifier: [ +number_modifier: [ | "(" "warning" "after" bignat ")" | "(" "abstract" "after" bignat ")" ] |