From 754e138e1e1c86dcd5e9d07084a5d33a5056ce9d Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 4 Sep 2020 15:09:00 +0200
Subject: [refman] Rename numeral to number

---
 doc/tools/docgram/common.edit_mlg |  4 ++--
 doc/tools/docgram/orderedGrammar  | 10 +++++-----
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'doc/tools')

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: [
-- 
cgit v1.2.3