aboutsummaryrefslogtreecommitdiff
path: root/parsing/cLexer.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-09-12 20:00:32 +0000
committerGitHub2020-09-12 20:00:32 +0000
commite0696ef1db06dbe32c95ac16b9c54d6b3624dff0 (patch)
treeb4c98d06350c274b46951470ab48aec11dbf35fa /parsing/cLexer.ml
parent5b62a6908202eef2c40d2f4989d8d21d0f6c3e16 (diff)
parentad7140a7127b147caf20d7c3803b918e3c6776f5 (diff)
Merge PR #12979: Uniformize names for number literals between parsing and refman
Reviewed-by: herbelin Reviewed-by: jfehrle Ack-by: Zimmi48 Ack-by: proux01
Diffstat (limited to 'parsing/cLexer.ml')
-rw-r--r--parsing/cLexer.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index 85640cabba..a98cf3b7de 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -710,7 +710,7 @@ let rec next_token ~diff_mode loc s =
let n = NumTok.Unsigned.parse s in
let ep = Stream.count s in
comment_stop bp;
- (NUMERAL n, set_loc_pos loc bp ep)
+ (NUMBER n, set_loc_pos loc bp ep)
| Some '\"' ->
Stream.junk s;
let (loc, len) =
@@ -796,8 +796,8 @@ let token_text : type c. c Tok.p -> string = function
| PKEYWORD t -> "'" ^ t ^ "'"
| PIDENT None -> "identifier"
| PIDENT (Some t) -> "'" ^ t ^ "'"
- | PNUMERAL None -> "numeral"
- | PNUMERAL (Some n) -> "'" ^ NumTok.Unsigned.sprint n ^ "'"
+ | PNUMBER None -> "numeral"
+ | PNUMBER (Some n) -> "'" ^ NumTok.Unsigned.sprint n ^ "'"
| PSTRING None -> "string"
| PSTRING (Some s) -> "STRING \"" ^ s ^ "\""
| PLEFTQMARK -> "LEFTQMARK"
@@ -891,5 +891,5 @@ let terminal s =
(* Precondition: the input is a numeral (c.f. [NumTok.t]) *)
let terminal_numeral s = match NumTok.Unsigned.parse_string s with
- | Some n -> PNUMERAL (Some n)
+ | Some n -> PNUMBER (Some n)
| None -> failwith "numeral token expected."