Renaming Numeral into Number

3 files changed, 14 insertions, 14 deletions

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: