aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_main.ml2
-rw-r--r--parsing/cLexer.ml8
-rw-r--r--parsing/g_constr.mlg4
-rw-r--r--parsing/g_prim.mlg8
-rw-r--r--parsing/tok.ml16
-rw-r--r--parsing/tok.mli4
-rw-r--r--plugins/ltac/g_tactic.mlg2
-rw-r--r--plugins/ssr/ssrparser.mlg8
-rw-r--r--vernac/g_vernac.mlg8
9 files changed, 30 insertions, 30 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index baa6c2d64e..fce4db1869 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -225,7 +225,7 @@ function
| "IDENT", s -> fprintf fmt "Tok.PIDENT (%a)" print_pat s
| "PATTERNIDENT", s -> fprintf fmt "Tok.PPATTERNIDENT (%a)" print_pat s
| "FIELD", s -> fprintf fmt "Tok.PFIELD (%a)" print_pat s
-| "INT", s -> fprintf fmt "Tok.PINT (%a)" print_pat s
+| "NUMERAL", s -> fprintf fmt "Tok.PNUMERAL (%a)" print_pat s
| "STRING", s -> fprintf fmt "Tok.PSTRING (%a)" print_pat s
| "LEFTQMARK", None -> fprintf fmt "Tok.PLEFTQMARK"
| "BULLET", s -> fprintf fmt "Tok.PBULLET (%a)" print_pat s
diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml
index b81d89edf9..f2e51afff5 100644
--- a/parsing/cLexer.ml
+++ b/parsing/cLexer.ml
@@ -714,7 +714,7 @@ let rec next_token ~diff_mode loc s =
in
let ep = Stream.count s in
comment_stop bp;
- (INT (get_buff len), set_loc_pos loc bp ep)
+ (NUMERAL (get_buff len), 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 ^ "'"
- | PINT None -> "integer"
- | PINT (Some s) -> "'" ^ s ^ "'"
+ | PNUMERAL None -> "integer"
+ | PNUMERAL (Some s) -> "'" ^ s ^ "'"
| PSTRING None -> "string"
| PSTRING (Some s) -> "STRING \"" ^ s ^ "\""
| PLEFTQMARK -> "LEFTQMARK"
@@ -875,5 +875,5 @@ let terminal s =
let s = strip s in
let () = match s with "" -> failwith "empty token." | _ -> () in
if is_ident_not_keyword s then PIDENT (Some s)
- else if is_number s then PINT (Some s)
+ else if is_number s then PNUMERAL (Some s)
else PKEYWORD s
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 9679474e81..0586dda555 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -305,7 +305,7 @@ GRAMMAR EXTEND Gram
atomic_constr:
[ [ g=global; i=instance -> { CAst.make ~loc @@ CRef (g,i) }
| s=sort -> { CAst.make ~loc @@ CSort s }
- | n=INT -> { CAst.make ~loc @@ CPrim (Numeral (SPlus,n)) }
+ | n=NUMERAL-> { CAst.make ~loc @@ CPrim (Numeral (SPlus,n)) }
| s=string -> { CAst.make ~loc @@ CPrim (String s) }
| "_" -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) }
| "?"; "["; id=ident; "]" -> { CAst.make ~loc @@ CHole (None, IntroIdentifier id, None) }
@@ -424,7 +424,7 @@ GRAMMAR EXTEND Gram
| _ -> p
in
CAst.make ~loc @@ CPatCast (p, ty) }
- | n = INT -> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) }
+ | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) }
| s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ]
;
impl_ident_tail:
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 6247a12640..9c5fe2a71d 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -110,13 +110,13 @@ GRAMMAR EXTEND Gram
[ [ s = string -> { CAst.make ~loc s } ] ]
;
integer:
- [ [ i = INT -> { my_int_of_string loc i }
- | "-"; i = INT -> { - my_int_of_string loc i } ] ]
+ [ [ i = NUMERAL -> { my_int_of_string loc i }
+ | "-"; i = NUMERAL -> { - my_int_of_string loc i } ] ]
;
natural:
- [ [ i = INT -> { my_int_of_string loc i } ] ]
+ [ [ i = NUMERAL -> { my_int_of_string loc i } ] ]
;
bigint: (* Negative numbers are dealt with elsewhere *)
- [ [ i = INT -> { i } ] ]
+ [ [ i = NUMERAL -> { i } ] ]
;
END
diff --git a/parsing/tok.ml b/parsing/tok.ml
index 186d0502fc..36d319d543 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -17,7 +17,7 @@ type 'c p =
| PPATTERNIDENT : string option -> string p
| PIDENT : string option -> string p
| PFIELD : string option -> string p
- | PINT : string option -> string p
+ | PNUMERAL : string option -> string p
| PSTRING : string option -> string p
| PLEFTQMARK : unit p
| PBULLET : string option -> string p
@@ -30,7 +30,7 @@ let pattern_strings : type c. c p -> string * string option =
| PPATTERNIDENT s -> "PATTERNIDENT", s
| PIDENT s -> "IDENT", s
| PFIELD s -> "FIELD", s
- | PINT s -> "INT", s
+ | PNUMERAL s -> "INT", s
| PSTRING s -> "STRING", s
| PLEFTQMARK -> "LEFTQMARK", None
| PBULLET s -> "BULLET", s
@@ -42,7 +42,7 @@ type t =
| PATTERNIDENT of string
| IDENT of string
| FIELD of string
- | INT of string
+ | NUMERAL of string
| STRING of string
| LEFTQMARK
| BULLET of string
@@ -57,7 +57,7 @@ let equal_p (type a b) (t1 : a p) (t2 : b p) : (a, b) Util.eq option =
| PPATTERNIDENT s1, PPATTERNIDENT s2 when streq s1 s2 -> Some Util.Refl
| PIDENT s1, PIDENT s2 when streq s1 s2 -> Some Util.Refl
| PFIELD s1, PFIELD s2 when streq s1 s2 -> Some Util.Refl
- | PINT s1, PINT s2 when streq s1 s2 -> Some Util.Refl
+ | PNUMERAL s1, PNUMERAL s2 when streq s1 s2 -> Some Util.Refl
| PSTRING s1, PSTRING s2 when streq s1 s2 -> Some Util.Refl
| PLEFTQMARK, PLEFTQMARK -> Some Util.Refl
| PBULLET s1, PBULLET s2 when streq s1 s2 -> Some Util.Refl
@@ -71,7 +71,7 @@ let equal t1 t2 = match t1, t2 with
| PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2
| IDENT s1, IDENT s2 -> string_equal s1 s2
| FIELD s1, FIELD s2 -> string_equal s1 s2
-| INT s1, INT s2 -> string_equal s1 s2
+| NUMERAL s1, NUMERAL s2 -> string_equal s1 s2
| STRING s1, STRING s2 -> string_equal s1 s2
| LEFTQMARK, LEFTQMARK -> true
| BULLET s1, BULLET s2 -> string_equal s1 s2
@@ -98,7 +98,7 @@ let extract_string diff_mode = function
else s
| PATTERNIDENT s -> s
| FIELD s -> if diff_mode then "." ^ s else s
- | INT s -> s
+ | NUMERAL s -> s
| LEFTQMARK -> "?"
| BULLET s -> s
| QUOTATION(_,s) -> s
@@ -129,8 +129,8 @@ let match_pattern (type c) (p : c p) : t -> c =
| PPATTERNIDENT (Some s) -> (function PATTERNIDENT s' when seq s s' -> s' | _ -> err ())
| PFIELD None -> (function FIELD s -> s | _ -> err ())
| PFIELD (Some s) -> (function FIELD s' when seq s s' -> s' | _ -> err ())
- | PINT None -> (function INT s -> s | _ -> err ())
- | PINT (Some s) -> (function INT s' when seq s s' -> s' | _ -> err ())
+ | PNUMERAL None -> (function NUMERAL s -> s | _ -> err ())
+ | PNUMERAL (Some s) -> (function NUMERAL s' when seq s s' -> s' | _ -> err ())
| PSTRING None -> (function STRING s -> s | _ -> err ())
| PSTRING (Some s) -> (function STRING s' when seq s s' -> s' | _ -> err ())
| PLEFTQMARK -> (function LEFTQMARK -> () | _ -> err ())
diff --git a/parsing/tok.mli b/parsing/tok.mli
index 678877720d..2b3bb85174 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -15,7 +15,7 @@ type 'c p =
| PPATTERNIDENT : string option -> string p
| PIDENT : string option -> string p
| PFIELD : string option -> string p
- | PINT : string option -> string p
+ | PNUMERAL : string option -> string p
| PSTRING : string option -> string p
| PLEFTQMARK : unit p
| PBULLET : string option -> string p
@@ -29,7 +29,7 @@ type t =
| PATTERNIDENT of string
| IDENT of string
| FIELD of string
- | INT of string
+ | NUMERAL of string
| STRING of string
| LEFTQMARK
| BULLET of string
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 574e22d50e..90dda4850e 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -72,7 +72,7 @@ let test_lpar_idnum_coloneq =
match stream_nth 0 strm with
| KEYWORD "(" ->
(match stream_nth 1 strm with
- | IDENT _ | INT _ ->
+ | IDENT _ | NUMERAL _ ->
(match stream_nth 2 strm with
| KEYWORD ":=" -> ()
| _ -> err ())
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 9931305832..457b333a16 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -224,20 +224,20 @@ let test_ssrslashnum b1 b2 strm =
match Util.stream_nth 0 strm with
| Tok.KEYWORD "/" ->
(match Util.stream_nth 1 strm with
- | Tok.INT _ when b1 ->
+ | Tok.NUMERAL _ when b1 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" | Tok.KEYWORD "/=" when not b2 -> ()
| Tok.KEYWORD "/" ->
if not b2 then () else begin
match Util.stream_nth 3 strm with
- | Tok.INT _ -> ()
+ | Tok.NUMERAL _ -> ()
| _ -> raise Stream.Failure
end
| _ -> raise Stream.Failure)
| Tok.KEYWORD "/" when not b1 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" when not b2 -> ()
- | Tok.INT _ when b2 ->
+ | Tok.NUMERAL _ when b2 ->
(match Util.stream_nth 3 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
@@ -248,7 +248,7 @@ let test_ssrslashnum b1 b2 strm =
| Tok.KEYWORD "//" when not b1 ->
(match Util.stream_nth 1 strm with
| Tok.KEYWORD "=" when not b2 -> ()
- | Tok.INT _ when b2 ->
+ | Tok.NUMERAL _ when b2 ->
(match Util.stream_nth 2 strm with
| Tok.KEYWORD "=" -> ()
| _ -> raise Stream.Failure)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 589b15fd41..d80f29cf1b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -294,7 +294,7 @@ GRAMMAR EXTEND Gram
| IDENT "Conjectures" -> { ("Conjectures", (NoDischarge, Conjectural)) } ] ]
;
inline:
- [ [ IDENT "Inline"; "("; i = INT; ")" -> { InlineAt (int_of_string i) }
+ [ [ IDENT "Inline"; "("; i = NUMERAL; ")" -> { InlineAt (int_of_string i) }
| IDENT "Inline" -> { DefaultInline }
| -> { NoInline } ] ]
;
@@ -607,7 +607,7 @@ GRAMMAR EXTEND Gram
| -> { [] } ] ]
;
functor_app_annot:
- [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" ->
+ [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = NUMERAL; "]" ->
{ InlineAt (int_of_string i) }
| "["; IDENT "no"; IDENT "inline"; "]" -> { NoInline }
| -> { DefaultInline }
@@ -847,8 +847,8 @@ GRAMMAR EXTEND Gram
strategy_level:
[ [ IDENT "expand" -> { Conv_oracle.Expand }
| IDENT "opaque" -> { Conv_oracle.Opaque }
- | n=INT -> { Conv_oracle.Level (int_of_string n) }
- | "-"; n=INT -> { Conv_oracle.Level (- int_of_string n) }
+ | n=NUMERAL -> { Conv_oracle.Level (int_of_string n) }
+ | "-"; n=NUMERAL -> { Conv_oracle.Level (- int_of_string n) }
| IDENT "transparent" -> { Conv_oracle.transparent } ] ]
;
instance_name:
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:03:49 +0000