diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/cLexer.ml | 8 | ||||
| -rw-r--r-- | parsing/cLexer.mli | 4 | ||||
| -rw-r--r-- | parsing/g_constr.mlg | 16 |
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: |