Renaming numnotoption into number_modifier

3 files changed, 23 insertions, 23 deletions

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