Renaming numnotoption into number_modifier

4 files changed, 16 insertions, 15 deletions

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index f982898335..a36772b2d7 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1553,16 +1553,16 @@ numbers (see :ref:`datatypes`).
 Number notations
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print : @scope_name {? @numeral_modifier }
+.. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print : @scope_name {? @number_modifier }
    :name: Number Notation
 
-   .. insertprodn numeral_modifier numeral_modifier
+   .. insertprodn number_modifier number_modifier
 
    .. prodn::
-      numeral_modifier ::= ( warning after @bignat )
+      number_modifier ::= ( warning after @bignat )
       | ( abstract after @bignat )
 
-   This command allows the user to customize the way numeral literals
+   This command allows the user to customize the way number literals
    are parsed and printed.
 
       :n:`@qualid__type`
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index f6a684bbd7..5d0f9208fc 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1285,10 +1285,10 @@ command: [
 | WITH "Declare" "Scope" scope_name
 
 (* odd that these are in command while other notation-related ones are in syntax *)
-| REPLACE "Numeral" "Notation" reference reference reference ":" ident numeral_modifier
-| WITH "Numeral" "Notation" reference reference reference ":" scope_name numeral_modifier
-| REPLACE "Number" "Notation" reference reference reference ":" ident numeral_modifier
-| WITH "Number" "Notation" reference reference reference ":" scope_name numeral_modifier
+| REPLACE "Numeral" "Notation" reference reference reference ":" ident number_modifier
+| WITH "Numeral" "Notation" reference reference reference ":" scope_name number_modifier
+| REPLACE "Number" "Notation" reference reference reference ":" ident number_modifier
+| WITH "Number" "Notation" reference reference reference ":" scope_name number_modifier
 | REPLACE "String" "Notation" reference reference reference ":" ident
 | WITH "String" "Notation" reference reference reference ":" scope_name
 
@@ -1358,7 +1358,7 @@ explicit_subentry: [
 | DELETE "constr"    (* covered by another prod *)
 ]
 
-numeral_modifier: [
+number_modifier: [
 | OPTINREF
 ]
 
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index c764cb6f37..914347b4cf 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -686,8 +686,8 @@ command: [
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" ident ":" constr OPT field_mods      (* ring plugin *)
 | "Print" "Fields"      (* ring plugin *)
-| "Number" "Notation" reference reference reference ":" ident numeral_modifier
-| "Numeral" "Notation" reference reference reference ":" ident numeral_modifier
+| "Number" "Notation" reference reference reference ":" ident number_modifier
+| "Numeral" "Notation" reference reference reference ":" ident number_modifier
 | "String" "Notation" reference reference reference ":" ident
 | "Ltac2" ltac2_entry      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr6      (* Ltac2 plugin *)
@@ -2549,7 +2549,7 @@ field_mods: [
 | "(" LIST1 field_mod SEP "," ")"      (* ring plugin *)
 ]
 
-numeral_modifier: [
+number_modifier: [
 |
 | "(" "warning" "after" bignat ")"
 | "(" "abstract" "after" bignat ")"
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 ")"
 ]