Rename the INT token to NUMERAL

In anticipation of future uses of this token for non integer numerals.

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: