Renaming Numeral into Number

17 files changed, 129 insertions, 129 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 83929bd030..8affe58824 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -454,7 +454,7 @@ struct
 
 let terminal s =
   let p =
-    if s <> "" && s.[0] >= '0' && s.[0] <= '9' then "CLexer.terminal_numeral"
+    if s <> "" && s.[0] >= '0' && s.[0] <= '9' then "CLexer.terminal_number"
     else "CLexer.terminal" in
   let c = Printf.sprintf "Pcoq.Symbol.token (%s \"%s\")" p s in
   SymbQuote c
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index d14d156ffc..235310660b 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -58,7 +58,7 @@ type abstraction_kind = AbsLambda | AbsPi
 type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
 
 type prim_token =
-  | Numeral of NumTok.Signed.t
+  | Number of NumTok.Signed.t
   | String of string
 
 type instance_expr = Glob_term.glob_level list
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 7075d082ee..8cc63c5d03 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -44,13 +44,13 @@ let names_of_local_binders bl =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
-(* Note: redundant Numeral representations, such as -0 and +0 (and others),
+(* Note: redundant Number representations, such as -0 and +0 (and others),
    are considered different here. *)
 
 let prim_token_eq t1 t2 = match t1, t2 with
-| Numeral n1, Numeral n2 -> NumTok.Signed.equal n1 n2
+| Number n1, Number n2 -> NumTok.Signed.equal n1 n2
 | String s1, String s2 -> String.equal s1 s2
-| (Numeral _ | String _), _ -> false
+| (Number _ | String _), _ -> false
 
 let explicitation_eq ex1 ex2 = match ex1, ex2 with
 | ExplByPos (i1, id1), ExplByPos (i2, id2) ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7bf1c58148..d1bec16a3f 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -357,18 +357,18 @@ let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
 let make_notation_gen loc ntn mknot mkprim destprim l bl =
   match snd ntn,List.map destprim l with
     (* Special case to avoid writing "- 3" for e.g. (Z.opp 3) *)
-    | "- _", [Some (Numeral p)] when not (NumTok.Signed.is_zero p) ->
+    | "- _", [Some (Number p)] when not (NumTok.Signed.is_zero p) ->
         assert (bl=[]);
         mknot (loc,ntn,([mknot (loc,(InConstrEntry,"( _ )"),l,[])]),[])
     | _ ->
         match decompose_notation_key ntn, l with
         | (InConstrEntry,[Terminal "-"; Terminal x]), [] ->
            begin match NumTok.Unsigned.parse_string x with
-           | Some n -> mkprim (loc, Numeral (NumTok.SMinus,n))
+           | Some n -> mkprim (loc, Number (NumTok.SMinus,n))
            | None -> mknot (loc,ntn,l,bl) end
         | (InConstrEntry,[Terminal x]), [] ->
            begin match NumTok.Unsigned.parse_string x with
-           | Some n -> mkprim (loc, Numeral (NumTok.SPlus,n))
+           | Some n -> mkprim (loc, Number (NumTok.SPlus,n))
            | None -> mknot (loc,ntn,l,bl) end
         | _ -> mknot (loc,ntn,l,bl)
 
@@ -915,7 +915,7 @@ let extern_float f scopes =
       let hex = !Flags.raw_print || not (get_printing_float ()) in
       if hex then Float64.to_hex_string f else Float64.to_string f in
     let n = NumTok.Signed.of_string s in
-    extern_prim_token_delimiter_if_required (Numeral n)
+    extern_prim_token_delimiter_if_required (Number n)
       "float" "float_scope" scopes
 
 (**********************************************************************)
@@ -1097,7 +1097,7 @@ let rec extern inctx ?impargs scopes vars r =
 
   | GInt i ->
      extern_prim_token_delimiter_if_required
-       (Numeral (NumTok.Signed.of_int_string (Uint63.to_string i)))
+       (Number (NumTok.Signed.of_int_string (Uint63.to_string i)))
        "int63" "int63_scope" (snd scopes)
 
   | GFloat f -> extern_float f (snd scopes)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 959b61a3d7..5fb6664dd6 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1570,11 +1570,11 @@ let rec subst_pat_iterator y t = DAst.(map (function
   | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
 
 let is_non_zero c = match c with
-| { CAst.v = CPrim (Numeral p) } -> not (NumTok.Signed.is_zero p)
+| { CAst.v = CPrim (Number p) } -> not (NumTok.Signed.is_zero p)
 | _ -> false
 
 let is_non_zero_pat c = match c with
-| { CAst.v = CPatPrim (Numeral p) } -> not (NumTok.Signed.is_zero p)
+| { CAst.v = CPatPrim (Number p) } -> not (NumTok.Signed.is_zero p)
 | _ -> false
 
 let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
@@ -1689,8 +1689,8 @@ let drop_notations_pattern looked_for genv =
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
         DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
     | CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a ->
-      let p = match a.CAst.v with CPatPrim (Numeral (_, p)) -> p | _ -> assert false in
-      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (SMinus,p)) scopes in
+      let p = match a.CAst.v with CPatPrim (Number (_, p)) -> p | _ -> assert false in
+      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Number (SMinus,p)) scopes in
       rcp_of_glob scopes pat
     | CPatNotation (_,(InConstrEntry,"( _ )"),([a],[]),[]) ->
       in_pat top scopes a
@@ -2006,8 +2006,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         GLetIn (na.CAst.v, inc1, int,
           intern_restart_binders (push_name_env ntnvars (impls_term_list 1 inc1) env na) c2)
     | CNotation (_,(InConstrEntry,"- _"), ([a],[],[],[])) when is_non_zero a ->
-      let p = match a.CAst.v with CPrim (Numeral (_, p)) -> p | _ -> assert false in
-       intern env (CAst.make ?loc @@ CPrim (Numeral (SMinus,p)))
+      let p = match a.CAst.v with CPrim (Number (_, p)) -> p | _ -> assert false in
+       intern env (CAst.make ?loc @@ CPrim (Number (SMinus,p)))
     | CNotation (_,(InConstrEntry,"( _ )"),([a],[],[],[])) -> intern env a
     | CNotation (_,ntn,args) ->
         let c = intern_notation intern env ntnvars loc ntn args in
diff --git a/interp/notation.ml b/interp/notation.ml
index 269e20c16e..8a35eeb203 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -32,7 +32,7 @@ open NumTok
     fail if a number has no interpretation in the scope (e.g. there is
     no interpretation for negative numbers in [nat]); interpreters both for
     terms and patterns can be set; these interpreters are in permanent table
-    [numeral_interpreter_tab]
+    [number_interpreter_tab]
   - a set of ML printers for expressions denoting numbers parsable in
     this scope
   - a set of interpretations for infix (more generally distfix) notations
@@ -446,13 +446,13 @@ module InnerPrimToken = struct
 
   let do_interp ?loc interp primtok =
     match primtok, interp with
-    | Numeral n, RawNumInterp interp -> interp ?loc n
-    | Numeral n, BigNumInterp interp ->
+    | Number n, RawNumInterp interp -> interp ?loc n
+    | Number n, BigNumInterp interp ->
       (match NumTok.Signed.to_bigint n with
        | Some n -> interp ?loc n
        | None -> raise Not_found)
     | String s, StringInterp interp -> interp ?loc s
-    | (Numeral _ | String _),
+    | (Number _ | String _),
       (RawNumInterp _ | BigNumInterp _ | StringInterp _) -> raise Not_found
 
   type uninterpreter =
@@ -466,16 +466,16 @@ module InnerPrimToken = struct
     | StringUninterp f, StringUninterp f' -> f == f'
     | _ -> false
 
-  let mkNumeral n =
-    Numeral (NumTok.Signed.of_bigint CDec n)
+  let mkNumber n =
+    Number (NumTok.Signed.of_bigint CDec n)
 
   let mkString = function
     | None -> None
     | Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
   let do_uninterp uninterp g = match uninterp with
-    | RawNumUninterp u -> Option.map (fun (s,n) -> Numeral (s,n)) (u g)
-    | BigNumUninterp u -> Option.map mkNumeral (u g)
+    | RawNumUninterp u -> Option.map (fun (s,n) -> Number (s,n)) (u g)
+    | BigNumUninterp u -> Option.map mkNumber (u g)
     | StringUninterp u -> mkString (u g)
 
 end
@@ -495,7 +495,7 @@ let prim_token_uninterpreters =
   (Hashtbl.create 7 : (prim_token_uid, InnerPrimToken.uninterpreter) Hashtbl.t)
 
 (*******************************************************)
-(* Numeral notation interpretation                     *)
+(* Number notation interpretation                      *)
 type prim_token_notation_error =
   | UnexpectedTerm of Constr.t
   | UnexpectedNonOptionTerm of Constr.t
@@ -519,21 +519,21 @@ type z_pos_ty =
   { z_ty : Names.inductive;
     pos_ty : Names.inductive }
 
-type numeral_ty =
+type number_ty =
   { int : int_ty;
     decimal : Names.inductive;
     hexadecimal : Names.inductive;
-    numeral : Names.inductive }
+    number : Names.inductive }
 
 type target_kind =
-  | Int of int_ty (* Coq.Init.Numeral.int + uint *)
-  | UInt of int_ty (* Coq.Init.Numeral.uint *)
+  | Int of int_ty (* Coq.Init.Number.int + uint *)
+  | UInt of int_ty (* Coq.Init.Number.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
-  | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *)
+  | Number of number_ty (* Coq.Init.Number.number + uint + int *)
   | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
   | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
-  | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
+  | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
 
 type string_target_kind =
   | ListByte
@@ -550,11 +550,11 @@ type ('target, 'warning) prim_token_notation_obj =
     ty_name : Libnames.qualid; (* for warnings / error messages *)
     warning : 'warning }
 
-type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
 type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
 
 module PrimTokenNotation = struct
-(** * Code shared between Numeral notation and String notation *)
+(** * Code shared between Number notation and String notation *)
 (** Reduction
 
     The constr [c] below isn't necessarily well-typed, since we
@@ -588,7 +588,7 @@ exception NotAValidPrimToken
     to [constr] for the subset that concerns us.
 
     Note that if you update [constr_of_glob], you should update the
-    corresponding numeral notation *and* string notation doc in
+    corresponding number notation *and* string notation doc in
     doc/sphinx/user-extensions/syntax-extensions.rst that describes
     what it means for a term to be ground / to be able to be
     considered for parsing. *)
@@ -670,8 +670,8 @@ let rec int63_of_pos_bigint i =
       (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo))
     else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)
 
-module Numeral = struct
-(** * Numeral notation *)
+module Numbers = struct
+(** * Number notation *)
 open PrimTokenNotation
 
 let warn_large_num =
@@ -727,7 +727,7 @@ let coqint_of_rawnum inds c (sign,n) =
   let pos_neg = match sign with SPlus -> 1 | SMinus -> 2 in
   mkApp (mkConstruct (ind, pos_neg), [|uint|])
 
-let coqnumeral_of_rawnum inds c n =
+let coqnumber_of_rawnum inds c n =
   let ind = match c with CDec -> inds.decimal | CHex -> inds.hexadecimal in
   let i, f, e = NumTok.Signed.to_int_frac_and_exponent n in
   let i = coqint_of_rawnum inds.int c i in
@@ -744,14 +744,14 @@ let mkDecHex ind c n = match c with
 
 exception NonDecimal
 
-let decimal_coqnumeral_of_rawnum inds n =
+let decimal_coqnumber_of_rawnum inds n =
   if NumTok.Signed.classify n <> CDec then raise NonDecimal;
-  coqnumeral_of_rawnum inds CDec n
+  coqnumber_of_rawnum inds CDec n
 
-let coqnumeral_of_rawnum inds n =
+let coqnumber_of_rawnum inds n =
   let c = NumTok.Signed.classify n in
-  let n = coqnumeral_of_rawnum inds c n in
-  mkDecHex inds.numeral c n
+  let n = coqnumber_of_rawnum inds c n in
+  mkDecHex inds.number c n
 
 let decimal_coquint_of_rawnum inds n =
   if NumTok.UnsignedNat.classify n <> CDec then raise NonDecimal;
@@ -801,7 +801,7 @@ let rawnum_of_coqint cl c =
       | _ -> raise NotAValidPrimToken)
   | _ -> raise NotAValidPrimToken
 
-let rawnum_of_coqnumeral cl c =
+let rawnum_of_coqnumber cl c =
   let of_ife i f e =
     let n = rawnum_of_coqint cl i in
     let f = try Some (rawnum_of_coquint cl f) with NotAValidPrimToken -> None in
@@ -820,12 +820,12 @@ let destDecHex c = match Constr.kind c with
       | _ -> raise NotAValidPrimToken)
   | _ -> raise NotAValidPrimToken
 
-let decimal_rawnum_of_coqnumeral c =
-  rawnum_of_coqnumeral CDec c
+let decimal_rawnum_of_coqnumber c =
+  rawnum_of_coqnumber CDec c
 
-let rawnum_of_coqnumeral c =
+let rawnum_of_coqnumber c =
   let cl, c = destDecHex c in
-  rawnum_of_coqnumeral cl c
+  rawnum_of_coqnumber cl c
 
 let decimal_rawnum_of_coquint c =
   rawnum_of_coquint CDec c
@@ -947,9 +947,9 @@ let interp o ?loc n =
        interp_int63 ?loc (NumTok.SignedNat.to_bigint n)
     | (Int _ | UInt _ | DecimalInt _ | DecimalUInt _ | Z _ | Int63), _ ->
        no_such_prim_token "number" ?loc o.ty_name
-    | Numeral numeral_ty, _ -> coqnumeral_of_rawnum numeral_ty n
-    | Decimal numeral_ty, _ ->
-       (try decimal_coqnumeral_of_rawnum numeral_ty n
+    | Number number_ty, _ -> coqnumber_of_rawnum number_ty n
+    | Decimal number_ty, _ ->
+       (try decimal_coqnumber_of_rawnum number_ty n
         with NonDecimal -> no_such_prim_token "number" ?loc o.ty_name)
   in
   let env = Global.env () in
@@ -959,12 +959,12 @@ let interp o ?loc n =
   match o.warning, snd o.to_kind with
   | Abstract threshold, Direct when NumTok.Signed.is_bigger_int_than n threshold ->
      warn_abstract_large_num (o.ty_name,o.to_ty);
-     glob_of_constr "numeral" ?loc env sigma (mkApp (to_ty,[|c|]))
+     glob_of_constr "number" ?loc env sigma (mkApp (to_ty,[|c|]))
   | _ ->
      let res = eval_constr_app env sigma to_ty c in
      match snd o.to_kind with
-     | Direct -> glob_of_constr "numeral" ?loc env sigma res
-     | Option -> interp_option "number" "numeral" o.ty_name ?loc env sigma res
+     | Direct -> glob_of_constr "number" ?loc env sigma res
+     | Option -> interp_option "number" "number" o.ty_name ?loc env sigma res
 
 let uninterp o n =
   PrimTokenNotation.uninterp
@@ -973,10 +973,10 @@ let uninterp o n =
       | (UInt _, c) -> NumTok.Signed.of_nat (rawnum_of_coquint c)
       | (Z _, c) -> NumTok.Signed.of_bigint CDec (bigint_of_z c)
       | (Int63, c) -> NumTok.Signed.of_bigint CDec (bigint_of_int63 c)
-      | (Numeral _, c) -> rawnum_of_coqnumeral c
+      | (Number _, c) -> rawnum_of_coqnumber c
       | (DecimalInt _, c) -> NumTok.Signed.of_int (decimal_rawnum_of_coqint c)
       | (DecimalUInt _, c) -> NumTok.Signed.of_nat (decimal_rawnum_of_coquint c)
-      | (Decimal _, c) -> decimal_rawnum_of_coqnumeral c
+      | (Decimal _, c) -> decimal_rawnum_of_coqnumber c
     end o n
 end
 
@@ -1081,21 +1081,21 @@ end
 
 (* A [prim_token_infos], which is synchronized with the document
    state, either contains a unique id pointing to an unsynchronized
-   prim token function, or a numeral notation object describing how to
+   prim token function, or a number notation object describing how to
    interpret and uninterpret.  We provide [prim_token_infos] because
    we expect plugins to provide their own interpretation functions,
-   rather than going through numeral notations, which are available as
+   rather than going through number notations, which are available as
    a vernacular. *)
 
 type prim_token_interp_info =
     Uid of prim_token_uid
-  | NumeralNotation of numeral_notation_obj
+  | NumberNotation of number_notation_obj
   | StringNotation of string_notation_obj
 
 type prim_token_infos = {
   pt_local : bool; (** Is this interpretation local? *)
   pt_scope : scope_name; (** Concerned scope *)
-  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a number notation object describing (un)interp functions *)
   pt_required : required_module; (** Module that should be loaded first *)
   pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
   pt_in_match : bool (** Is this prim token legal in match patterns ? *)
@@ -1119,7 +1119,7 @@ let hashtbl_check_and_set allow_overwrite uid f h eq =
    | _ ->
       user_err ~hdr:"prim_token_interpreter"
        (str "Unique identifier " ++ str uid ++
-        str " already used to register a numeral or string (un)interpreter.")
+        str " already used to register a number or string (un)interpreter.")
 
 let register_gen_interpretation allow_overwrite uid (interp, uninterp) =
   hashtbl_check_and_set
@@ -1220,7 +1220,7 @@ let check_required_module ?loc sc (sp,d) =
         (str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++
          str (List.last d) ++ str ".")
 
-(* Look if some notation or numeral printer in [scope] can be used in
+(* Look if some notation or number printer in [scope] can be used in
    the scope stack [scopes], and if yes, using delimiters or not *)
 
 let find_with_delimiters = function
@@ -1237,7 +1237,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
       | NotationInScope scope' when String.equal scope scope' ->
         Some (None,None)
       | _ ->
-        (* If the most recently open scope has a notation/numeral printer
+        (* If the most recently open scope has a notation/number printer
            but not the expected one then we need delimiters *)
         if find scope then
           find_with_delimiters ntn_scope
@@ -1375,8 +1375,8 @@ let find_notation ntn sc =
   | _ -> raise Not_found
 
 let notation_of_prim_token = function
-  | Constrexpr.Numeral (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
-  | Constrexpr.Numeral (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
+  | Constrexpr.Number (SPlus,n) -> InConstrEntry, NumTok.Unsigned.sprint n
+  | Constrexpr.Number (SMinus,n) -> InConstrEntry, "- "^NumTok.Unsigned.sprint n
   | String _ -> raise Not_found
 
 let find_prim_token check_allowed ?loc p sc =
@@ -1394,7 +1394,7 @@ let find_prim_token check_allowed ?loc p sc =
   check_required_module ?loc sc spdir;
   let interp = match info with
     | Uid uid -> Hashtbl.find prim_token_interpreters uid
-    | NumeralNotation o -> InnerPrimToken.RawNumInterp (Numeral.interp o)
+    | NumberNotation o -> InnerPrimToken.RawNumInterp (Numbers.interp o)
     | StringNotation o -> InnerPrimToken.StringInterp (Strings.interp o)
   in
   let pat = InnerPrimToken.do_interp ?loc interp p in
@@ -1411,8 +1411,8 @@ let interp_prim_token_gen ?loc g p local_scopes =
     let _, info = Exninfo.capture exn in
     user_err ?loc ~info ~hdr:"interp_prim_token"
     ((match p with
-      | Numeral _ ->
-         str "No interpretation for numeral " ++ pr_notation (notation_of_prim_token p)
+      | Number _ ->
+         str "No interpretation for number " ++ pr_notation (notation_of_prim_token p)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token ?loc =
@@ -1659,14 +1659,14 @@ let availability_of_prim_token n printer_scope local_scopes =
       let uid = snd (String.Map.find scope !prim_token_interp_infos) in
       let open InnerPrimToken in
       match n, uid with
-      | Constrexpr.Numeral _, NumeralNotation _ -> true
-      | _, NumeralNotation _ -> false
+      | Constrexpr.Number _, NumberNotation _ -> true
+      | _, NumberNotation _ -> false
       | String _, StringNotation _ -> true
       | _, StringNotation _ -> false
       | _, Uid uid ->
         let interp = Hashtbl.find prim_token_interpreters uid in
         match n, interp with
-        | Constrexpr.Numeral _, (RawNumInterp _ | BigNumInterp _) -> true
+        | Constrexpr.Number _, (RawNumInterp _ | BigNumInterp _) -> true
         | String _, StringInterp _ -> true
         | _ -> false
     with Not_found -> false
@@ -1681,7 +1681,7 @@ let rec find_uninterpretation need_delim def find = function
         def
   | OpenScopeItem scope :: scopes ->
       (try find need_delim scope
-       with Not_found -> find_uninterpretation need_delim def find scopes)  (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a numeral notation *)
+       with Not_found -> find_uninterpretation need_delim def find scopes)  (* TODO: here we should also update the need_delim list with all regular notations in scope [scope] that could shadow a number notation *)
   | LonelyNotationItem ntn::scopes ->
       find_uninterpretation (ntn::need_delim) def find scopes
 
@@ -1693,7 +1693,7 @@ let uninterp_prim_token c local_scopes =
        try
          let uninterp = match info with
            | Uid uid -> Hashtbl.find prim_token_uninterpreters uid
-           | NumeralNotation o -> InnerPrimToken.RawNumUninterp (Numeral.uninterp o)
+           | NumberNotation o -> InnerPrimToken.RawNumUninterp (Numbers.uninterp o)
            | StringNotation o -> InnerPrimToken.StringUninterp (Strings.uninterp o)
          in
          match InnerPrimToken.do_uninterp uninterp (AnyGlobConstr c) with
diff --git a/interp/notation.mli b/interp/notation.mli
index d744ff41d9..918744b66a 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -74,7 +74,7 @@ val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
 
 (** {6 Declare and uses back and forth an interpretation of primitive token } *)
 
-(** A numeral interpreter is the pair of an interpreter for **(hexa)decimal**
+(** A number interpreter is the pair of an interpreter for **(hexa)decimal**
    numbers in terms and an optional interpreter in pattern, if
    non integer or negative numbers are not supported, the interpreter
    must fail with an appropriate error message *)
@@ -84,7 +84,7 @@ type required_module = full_path * string list
 type rawnum = NumTok.Signed.t
 
 (** The unique id string below will be used to refer to a particular
-    registered interpreter/uninterpreter of numeral or string notation.
+    registered interpreter/uninterpreter of number or string notation.
     Using the same uid for different (un)interpreters will fail.
     If at most one interpretation of prim token is used per scope,
     then the scope name could be used as unique id. *)
@@ -106,7 +106,7 @@ val register_bignumeral_interpretation :
 val register_string_interpretation :
   ?allow_overwrite:bool -> prim_token_uid -> string prim_token_interpretation -> unit
 
-(** * Numeral notation *)
+(** * Number notation *)
 
 type prim_token_notation_error =
   | UnexpectedTerm of Constr.t
@@ -131,21 +131,21 @@ type z_pos_ty =
   { z_ty : Names.inductive;
     pos_ty : Names.inductive }
 
-type numeral_ty =
+type number_ty =
   { int : int_ty;
     decimal : Names.inductive;
     hexadecimal : Names.inductive;
-    numeral : Names.inductive }
+    number : Names.inductive }
 
 type target_kind =
-  | Int of int_ty (* Coq.Init.Numeral.int + uint *)
-  | UInt of int_ty (* Coq.Init.Numeral.uint *)
+  | Int of int_ty (* Coq.Init.Number.int + uint *)
+  | UInt of int_ty (* Coq.Init.Number.uint *)
   | Z of z_pos_ty (* Coq.Numbers.BinNums.Z and positive *)
   | Int63 (* Coq.Numbers.Cyclic.Int63.Int63.int *)
-  | Numeral of numeral_ty (* Coq.Init.Numeral.numeral + uint + int *)
+  | Number of number_ty (* Coq.Init.Number.number + uint + int *)
   | DecimalInt of int_ty (* Coq.Init.Decimal.int + uint (deprecated) *)
   | DecimalUInt of int_ty (* Coq.Init.Decimal.uint (deprecated) *)
-  | Decimal of numeral_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
+  | Decimal of number_ty (* Coq.Init.Decimal.Decimal + uint + int (deprecated) *)
 
 type string_target_kind =
   | ListByte
@@ -162,18 +162,18 @@ type ('target, 'warning) prim_token_notation_obj =
     ty_name : Libnames.qualid; (* for warnings / error messages *)
     warning : 'warning }
 
-type numeral_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
+type number_notation_obj = (target_kind, numnot_option) prim_token_notation_obj
 type string_notation_obj = (string_target_kind, unit) prim_token_notation_obj
 
 type prim_token_interp_info =
     Uid of prim_token_uid
-  | NumeralNotation of numeral_notation_obj
+  | NumberNotation of number_notation_obj
   | StringNotation of string_notation_obj
 
 type prim_token_infos = {
   pt_local : bool; (** Is this interpretation local? *)
   pt_scope : scope_name; (** Concerned scope *)
-  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a numeral notation object describing (un)interp functions *)
+  pt_interp_info : prim_token_interp_info; (** Unique id "pointing" to (un)interp functions, OR a number notation object describing (un)interp functions *)
   pt_required : required_module; (** Module that should be loaded first *)
   pt_refs : GlobRef.t list; (** Entry points during uninterpretation *)
   pt_in_match : bool (** Is this prim token legal in match patterns ? *)
diff --git a/interp/numTok.mli b/interp/numTok.mli
index bcfe663dd2..386a25f042 100644
--- a/interp/numTok.mli
+++ b/interp/numTok.mli
@@ -8,20 +8,20 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Numerals in different forms: signed or unsigned, possibly with
+(** Numbers in different forms: signed or unsigned, possibly with
     fractional part and exponent.
 
-    Numerals are represented using raw strings of (hexa)decimal
+    Numbers are represented using raw strings of (hexa)decimal
     literals and a separate sign flag.
 
     Note that this representation is not unique, due to possible
     multiple leading or trailing zeros, and -0 = +0, for instances.
-    The reason to keep the numeral exactly as it was parsed is that
-    specific notations can be declared for specific numerals
+    The reason to keep the number exactly as it was parsed is that
+    specific notations can be declared for specific numbers
     (e.g. [Notation "0" := False], or [Notation "00" := (nil,nil)], or
     [Notation "2e1" := ...]). Those notations override the generic
-    interpretation as numeral. So, one has to record the form of the
-    numeral which exactly matches the notation. *)
+    interpretation as number. So, one has to record the form of the
+    number which exactly matches the notation. *)
 
 type sign = SPlus | SMinus
 
@@ -44,7 +44,7 @@ sig
 
   val sprint : t -> string
   val print : t -> Pp.t
-    (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+    (** [sprint] and [print] returns the number as it was parsed, for printing *)
 
   val classify : t -> num_class
 
@@ -69,7 +69,7 @@ sig
   val to_bigint : t -> Z.t
 end
 
-(** {6 Unsigned decimal numerals } *)
+(** {6 Unsigned decimal numbers } *)
 
 module Unsigned :
 sig
@@ -80,12 +80,12 @@ sig
 
   val sprint : t -> string
   val print : t -> Pp.t
-    (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+    (** [sprint] and [print] returns the number as it was parsed, for printing *)
 
   val parse : char Stream.t -> t
-    (** Parse a positive Coq numeral.
+    (** Parse a positive Coq number.
         Precondition: the first char on the stream is already known to be a digit (\[0-9\]).
-        Precondition: at least two extra chars after the numeral to parse.
+        Precondition: at least two extra chars after the number to parse.
 
         The recognized syntax is:
         - integer part: \[0-9\]\[0-9_\]*
@@ -97,13 +97,13 @@ sig
         - exponent part: empty or \[pP\]\[+-\]?\[0-9\]\[0-9_\]* *)
 
   val parse_string : string -> t option
-    (** Parse the string as a non negative Coq numeral, if possible *)
+    (** Parse the string as a non negative Coq number, if possible *)
 
   val classify : t -> num_class
 
 end
 
-(** {6 Signed decimal numerals } *)
+(** {6 Signed decimal numbers } *)
 
 module Signed :
 sig
@@ -117,10 +117,10 @@ sig
 
   val sprint : t -> string
   val print : t -> Pp.t
-    (** [sprint] and [print] returns the numeral as it was parsed, for printing *)
+    (** [sprint] and [print] returns the number as it was parsed, for printing *)
 
   val parse_string : string -> t option
-    (** Parse the string as a signed Coq numeral, if possible *)
+    (** Parse the string as a signed Coq number, if possible *)
 
   val of_int_string : string -> t
     (** Convert from a string in the syntax of OCaml's int/int64 *)
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index f485970eec..d8d2f2a2ef 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -823,7 +823,7 @@ let token_text : type c. c Tok.p -> string = function
   | PKEYWORD t -> "'" ^ t ^ "'"
   | PIDENT None -> "identifier"
   | PIDENT (Some t) -> "'" ^ t ^ "'"
-  | PNUMBER None -> "numeral"
+  | PNUMBER None -> "number"
   | PNUMBER (Some n) -> "'" ^ NumTok.Unsigned.sprint n ^ "'"
   | PSTRING None -> "string"
   | PSTRING (Some s) -> "STRING \"" ^ s ^ "\""
@@ -916,7 +916,7 @@ let terminal s =
   if is_ident_not_keyword s then PIDENT (Some s)
   else PKEYWORD s
 
-(* Precondition: the input is a numeral (c.f. [NumTok.t]) *)
-let terminal_numeral s = match NumTok.Unsigned.parse_string s with
+(* Precondition: the input is a number (c.f. [NumTok.t]) *)
+let terminal_number s = match NumTok.Unsigned.parse_string s with
   | Some n -> PNUMBER (Some n)
-  | None -> failwith "numeral token expected."
+  | None -> failwith "number token expected."
diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli
index ac2c5bcfe2..af4b7ba334 100644
--- a/parsing/cLexer.mli
+++ b/parsing/cLexer.mli
@@ -49,8 +49,8 @@ val check_keyword : string -> unit
 (** When string is not an ident, returns a keyword. *)
 val terminal : string -> string Tok.p
 
-(** Precondition: the input is a numeral (c.f. [NumTok.t]) *)
-val terminal_numeral : string -> NumTok.Unsigned.t Tok.p
+(** Precondition: the input is a number (c.f. [NumTok.t]) *)
+val terminal_number : string -> NumTok.Unsigned.t Tok.p
 
 (** The lexer of Coq: *)
 
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 349e14bba3..67a061175a 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -173,10 +173,10 @@ GRAMMAR EXTEND Gram
       [ c = atomic_constr -> { c }
       | c = term_match -> { c }
       | "("; c = term LEVEL "200"; ")" ->
-        { (* Preserve parentheses around numerals so that constrintern does not
-             collapse -(3) into the numeral -3. *)
+        { (* Preserve parentheses around numbers so that constrintern does not
+             collapse -(3) into the number -3. *)
           (match c.CAst.v with
-            | CPrim (Numeral (NumTok.SPlus,n)) ->
+            | CPrim (Number (NumTok.SPlus,n)) ->
                 CAst.make ~loc @@ CNotation(None,(InConstrEntry,"( _ )"),([c],[],[],[]))
             | _ -> c) }
       | "{|"; c = record_declaration; bar_cbrace -> { c }
@@ -258,7 +258,7 @@ GRAMMAR EXTEND Gram
   atomic_constr:
     [ [ g = global; i = univ_annot -> { CAst.make ~loc @@ CRef (g,i) }
       | s = sort   -> { CAst.make ~loc @@  CSort s }
-      | n = NUMBER-> { CAst.make ~loc @@ CPrim (Numeral (NumTok.SPlus,n)) }
+      | n = NUMBER-> { CAst.make ~loc @@ CPrim (Number (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPrim (String s) }
       | "_"      -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
       | "?"; "["; id = identref; "]"  -> { CAst.make ~loc @@  CHole (None, IntroIdentifier id.CAst.v, None) }
@@ -362,15 +362,15 @@ GRAMMAR EXTEND Gram
       | "{|"; pat = record_patterns; bar_cbrace -> { CAst.make ~loc @@ CPatRecord pat }
       | "_" -> { CAst.make ~loc @@ CPatAtom None }
       | "("; p = pattern LEVEL "200"; ")" ->
-        { (* Preserve parentheses around numerals so that constrintern does not
-             collapse -(3) into the numeral -3. *)
+        { (* Preserve parentheses around numbers so that constrintern does not
+             collapse -(3) into the number -3. *)
           match p.CAst.v with
-          | CPatPrim (Numeral (NumTok.SPlus,n)) ->
+          | CPatPrim (Number (NumTok.SPlus,n)) ->
               CAst.make ~loc @@ CPatNotation(None,(InConstrEntry,"( _ )"),([p],[]),[])
           | _ -> p }
       | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" ->
         { CAst.make ~loc @@ CPatOr (p::pl) }
-      | n = NUMBER-> { CAst.make ~loc @@ CPatPrim (Numeral (NumTok.SPlus,n)) }
+      | n = NUMBER-> { CAst.make ~loc @@ CPatPrim (Number (NumTok.SPlus,n)) }
       | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
   ;
   fixannot:
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 97d75261c5..ecfe6c1664 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -121,8 +121,8 @@ let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
     end
   | _ -> ElimOnConstr clbind
 
-let mkNumeral n =
-  Numeral (NumTok.Signed.of_int_string (string_of_int n))
+let mkNumber n =
+  Number (NumTok.Signed.of_int_string (string_of_int n))
 
 let mkTacCase with_evar = function
   | [(clear,ElimOnConstr cl),(None,None),None],None ->
@@ -130,7 +130,7 @@ let mkTacCase with_evar = function
   (* Reinterpret numbers as a notation for terms *)
   | [(clear,ElimOnAnonHyp n),(None,None),None],None ->
       TacCase (with_evar,
-        (clear,(CAst.make @@ CPrim (mkNumeral n),
+        (clear,(CAst.make @@ CPrim (mkNumber n),
          NoBindings)))
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 35fecfb0a5..ccdf5fa68e 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -350,7 +350,7 @@ let interp_index ist gl idx =
         | Some c ->
           let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc (None, []) with
-          | Constrexpr.Numeral n, _ when NumTok.Signed.is_int n ->
+          | Constrexpr.Number n, _ when NumTok.Signed.is_int n ->
             int_of_string (NumTok.Signed.to_string n)
           | _ -> raise Not_found
           end
diff --git a/plugins/syntax/int63_syntax.ml b/plugins/syntax/int63_syntax.ml
index 5f4db8e800..73a9341145 100644
--- a/plugins/syntax/int63_syntax.ml
+++ b/plugins/syntax/int63_syntax.ml
@@ -50,7 +50,7 @@ let _ =
        enable_prim_token_interpretation
          { pt_local = false;
            pt_scope = int63_scope;
-           pt_interp_info = NumeralNotation o;
+           pt_interp_info = NumberNotation o;
            pt_required = (int63_path, int63_module);
            pt_refs = [];
            pt_in_match = false })
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 313798b102..8635f39f1a 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -90,7 +90,7 @@ let locate_number () =
         int = int_ty;
         decimal = unsafe_locate_ind q_dec;
         hexadecimal = unsafe_locate_ind q_hex;
-        numeral = unsafe_locate_ind q_num;
+        number = unsafe_locate_ind q_num;
       } in
     Some (int_ty, mkRefC q_int, mkRefC q_uint, mkRefC q_dint, mkRefC q_duint,
           num_ty, mkRefC q_num, mkRefC q_dec)
@@ -151,8 +151,8 @@ let vernac_number_notation local ty f g scope opts =
     | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
     | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint cty) -> UInt int_ty, Direct
     | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty, Option
-    | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Numeral num_ty, Direct
-    | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Numeral num_ty, Option
+    | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum cty) -> Number num_ty, Direct
+    | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma f (arrow cnum (opt cty)) -> Number num_ty, Option
     | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint cty) -> DecimalInt int_ty, Direct
     | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma f (arrow cint (opt cty)) -> DecimalInt int_ty, Option
     | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma f (arrow cuint cty) -> DecimalUInt int_ty, Direct
@@ -176,8 +176,8 @@ let vernac_number_notation local ty f g scope opts =
     | Some (int_ty, cint, _, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
     | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty cuint) -> UInt int_ty, Direct
     | Some (int_ty, _, cuint, _, _, _, _, _) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty, Option
-    | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Numeral num_ty, Direct
-    | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Numeral num_ty, Option
+    | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty cnum) -> Number num_ty, Direct
+    | Some (_, _, _, _, _, num_ty, cnum, _) when has_type env sigma g (arrow cty (opt cnum)) -> Number num_ty, Option
     | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty cint) -> DecimalInt int_ty, Direct
     | Some (int_ty, _, _, cint, _, _, _, _) when has_type env sigma g (arrow cty (opt cint)) -> DecimalInt int_ty, Option
     | Some (int_ty, _, _, _, cuint, _, _, _) when has_type env sigma g (arrow cty cuint) -> DecimalUInt int_ty, Direct
@@ -209,7 +209,7 @@ let vernac_number_notation local ty f g scope opts =
   let i =
        { pt_local = local;
          pt_scope = scope;
-         pt_interp_info = NumeralNotation o;
+         pt_interp_info = NumberNotation o;
          pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[];
          pt_refs = constructors;
          pt_in_match = true }
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 8da1d636f0..d762959ede 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -77,8 +77,8 @@ let tag_var = tag Tag.variable
     | LevelSome -> true
 
   let prec_of_prim_token = function
-    | Numeral (NumTok.SPlus,_) -> lposint
-    | Numeral (NumTok.SMinus,_) -> lnegint
+    | Number (NumTok.SPlus,_) -> lposint
+    | Number (NumTok.SMinus,_) -> lnegint
     | String _ -> latom
 
   let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps =
@@ -222,7 +222,7 @@ let tag_var = tag Tag.variable
     | t ->  str " :" ++ pr_sep_com (fun()->brk(1,4)) (pr ltop) t
 
   let pr_prim_token = function
-    | Numeral n -> NumTok.Signed.print n
+    | Number n -> NumTok.Signed.print n
     | String s -> qs s
 
   let pr_evar pr id l =
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 123ea2c24e..efe4e17d0b 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -408,8 +408,8 @@ match e with
 | TTClosedBinderList _ -> { subst with binderlists = List.flatten v :: subst.binderlists }
 | TTBigint ->
   begin match forpat with
-  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Numeral (NumTok.Signed.of_int_string v)))
-  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Numeral (NumTok.Signed.of_int_string v)))
+  | ForConstr ->  push_constr subst (CAst.make @@ CPrim (Number (NumTok.Signed.of_int_string v)))
+  | ForPattern -> push_constr subst (CAst.make @@ CPatPrim (Number (NumTok.Signed.of_int_string v)))
   end
 | TTReference ->
   begin match forpat with