diff options
| author | Pierre Roux | 2020-09-04 15:09:00 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:20:28 +0200 |
| commit | 754e138e1e1c86dcd5e9d07084a5d33a5056ce9d (patch) | |
| tree | 55772785eadac1c653f587f9d0338e5ba9c2dfdc /doc/tools/docgram | |
| parent | 46b9480a717d5ca78e354fa843f39eed87cb7b15 (diff) | |
[refman] Rename numeral to number
Diffstat (limited to 'doc/tools/docgram')
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 4 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 10 |
2 files changed, 7 insertions, 7 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index ff40555696..fbf83760ad 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -770,7 +770,7 @@ int: [ | OPT "-" natural ] -numeral: [ +number: [ | OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat ) | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat ) ] @@ -795,7 +795,7 @@ ident: [ ] NUMBER: [ -| numeral +| number ] (* todo: QUOTATION only used in a test suite .mlg files, is it documented/useful? *) diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 6d07f6b0c4..a021bdbec0 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -93,7 +93,7 @@ term_explicit: [ ] primitive_notations: [ -| numeral +| number | string ] @@ -129,7 +129,7 @@ type: [ | term ] -numeral: [ +number: [ | OPT "-" decnat OPT ( "." LIST1 [ digit | "_" ] ) OPT ( [ "e" | "E" ] OPT [ "+" | "-" ] decnat ) | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat ) ] @@ -429,7 +429,7 @@ pattern0: [ | "{|" LIST0 ( qualid ":=" pattern ) "|}" | "_" | "(" LIST1 pattern SEP "|" ")" -| numeral +| number | string ] @@ -1291,8 +1291,8 @@ field_mod: [ ] numeral_modifier: [ -| "(" "warning" "after" numeral ")" -| "(" "abstract" "after" numeral ")" +| "(" "warning" "after" number ")" +| "(" "abstract" "after" number ")" ] hints_path: [ |