Renaming numnotoption into number_modifier

7 files changed, 39 insertions, 38 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 ")"
 ]
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 93d91abea3..48e262c3ef 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -19,7 +19,7 @@ open Names
 open Stdarg
 open Pcoq.Prim
 
-let pr_numnot_option = function
+let pr_number_modifier = function
   | Nop -> mt ()
   | Warning n -> str "(warning after " ++ NumTok.UnsignedNat.print n ++ str ")"
   | Abstract n -> str "(abstract after " ++ NumTok.UnsignedNat.print n ++ str ")"
@@ -31,21 +31,21 @@ let warn_deprecated_numeral_notation =
 
 }
 
-VERNAC ARGUMENT EXTEND numeral_modifier
-  PRINTED BY { pr_numnot_option }
+VERNAC ARGUMENT EXTEND number_modifier
+  PRINTED BY { pr_number_modifier }
 | [ ] -> { Nop }
 | [ "(" "warning" "after" bignat(waft) ")" ] -> { Warning (NumTok.UnsignedNat.of_string waft) }
 | [ "(" "abstract" "after" bignat(n) ")" ] -> { Abstract (NumTok.UnsignedNat.of_string n) }
 END
 
-VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
+VERNAC COMMAND EXTEND NumberNotation CLASSIFIED AS SIDEFF
   | #[ locality = Attributes.locality; ] [ "Number" "Notation" reference(ty) reference(f) reference(g) ":"
-      ident(sc) numeral_modifier(o) ] ->
+      ident(sc) number_modifier(o) ] ->
 
-    { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
+    { vernac_number_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
   | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
-      ident(sc) numeral_modifier(o) ] ->
+      ident(sc) number_modifier(o) ] ->
 
     { warn_deprecated_numeral_notation ();
-      vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
+      vernac_number_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
 END
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index fbf43be91f..313798b102 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -16,7 +16,7 @@ open Constrexpr
 open Constrexpr_ops
 open Notation
 
-(** * Numeral notation *)
+(** * Number notation *)
 
 let warn_abstract_large_num_no_op =
   CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
@@ -55,7 +55,7 @@ let locate_z () =
     }, mkRefC q_z)
   else None
 
-let locate_numeral () =
+let locate_number () =
   let dint = "num.int.type" in
   let duint = "num.uint.type" in
   let dec = "num.decimal.type" in
@@ -111,27 +111,27 @@ let has_type env sigma f ty =
 
 let type_error_to f ty =
   CErrors.user_err
-    (pr_qualid f ++ str " should go from Numeral.int to " ++
+    (pr_qualid f ++ str " should go from Number.int to " ++
      pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
-     fnl () ++ str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).")
+     fnl () ++ str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).")
 
 let type_error_of g ty =
   CErrors.user_err
     (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
-     str " to Numeral.int or (option Numeral.int)." ++ fnl () ++
-     str "Instead of Numeral.int, the types Numeral.uint or Z or Int63.int or Numeral.numeral could be used (you may need to require BinNums or Numeral or Int63 first).")
+     str " to Number.int or (option Number.int)." ++ fnl () ++
+     str "Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first).")
 
 let warn_deprecated_decimal =
   CWarnings.create ~name:"decimal-numeral-notation" ~category:"deprecated"
     (fun () ->
-      strbrk "Deprecated Numeral Notation for Decimal.uint, \
-              Decimal.int or Decimal.decimal. Use Numeral.uint, \
-              Numeral.int or Numeral.numeral respectively.")
+      strbrk "Deprecated Number Notation for Decimal.uint, \
+              Decimal.int or Decimal.decimal. Use Number.uint, \
+              Number.int or Number.number respectively.")
 
-let vernac_numeral_notation local ty f g scope opts =
+let vernac_number_notation local ty f g scope opts =
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let num_ty = locate_numeral () in
+  let num_ty = locate_number () in
   let z_pos_ty = locate_z () in
   let int63_ty = locate_int63 () in
   let tyc = Smartlocate.global_inductive_with_alias ty in
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index 99252484b4..d5fe42b0b4 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -12,8 +12,8 @@ open Libnames
 open Vernacexpr
 open Notation
 
-(** * Numeral notation *)
+(** * Number notation *)
 
-val vernac_numeral_notation : locality_flag ->
-                              qualid -> qualid -> qualid ->
-                              Notation_term.scope_name -> numnot_option -> unit
+val vernac_number_notation : locality_flag ->
+                             qualid -> qualid -> qualid ->
+                             Notation_term.scope_name -> numnot_option -> unit