[refman] Rename int to integer

12 files changed, 79 insertions, 83 deletions

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index be513833ad..d248839fa0 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -111,11 +111,11 @@ Identifiers
   symbols and non-breaking space. :production:`unicode_id_part`
   non-exhaustively includes symbols for prime letters and subscripts.
 
-Numerals
-  Numerals are sequences of digits with an optional fractional part
+Numbers
+  Numbers are sequences of digits with an optional fractional part
   and exponent, optionally preceded by a minus sign. Hexadecimal numerals
   start with ``0x`` or ``0X``. :n:`@int` is an integer;
-  a numeral without fractional nor exponent parts. :n:`@natural` is a non-negative
+  a number without fractional nor exponent parts. :n:`@natural` is a non-negative
   integer.  Underscores embedded in the digits are ignored, for example
   ``1_000_000`` is the same as ``1000000``.
 
@@ -124,7 +124,7 @@ Numerals
   .. prodn::
      number ::= {? - } @decnat {? . {+ {| @digit | _ } } } {? {| e | E } {? {| + | - } } @decnat }
      | {? - } @hexnat {? . {+ {| @hexdigit | _ } } } {? {| p | P } {? {| + | - } } @decnat }
-     int ::= {? - } @natural
+     integer ::= {? - } @natural
      natural ::= {| @decnat | @hexnat }
      decnat ::= @digit {* {| @digit | _ } }
      digit ::= 0 .. 9
@@ -434,7 +434,7 @@ gray boxes after the labels "Flag", "Option" and "Table".  In the pdf,
 they appear after a boldface label.  They are listed in the
 :ref:`options_index`.
 
-.. cmd:: Set @setting_name {? {| @int | @string } }
+.. cmd:: Set @setting_name {? {| @integer | @string } }
    :name: Set
 
    If :n:`@setting_name` is a flag, no value may be provided; the flag
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 2bccfcd615..2a102adfcc 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -74,7 +74,7 @@ The constructs in :token:`ltac_expr` are :term:`left associative`.
    ltac_expr0 ::= ( @ltac_expr )
    | [> @for_each_goal ]
    | @tactic_atom
-   tactic_atom ::= @int
+   tactic_atom ::= @integer
    | @qualid
    | ()
 
@@ -188,7 +188,7 @@ examining the part at the end under "Entry tactic:tactic_arg".
         -
 
       * - ``integer``
-        - :token:`int`
+        - :token:`integer`
         - an integer
         -
 
@@ -876,7 +876,7 @@ Print/identity tactic: idtac
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 
-.. tacn:: idtac {* {| @ident | @string | @int } }
+.. tacn:: idtac {* {| @ident | @string | @integer } }
    :name: idtac
 
    Leaves the proof unchanged and prints the given tokens. Strings and integers are printed
@@ -888,7 +888,7 @@ Print/identity tactic: idtac
 Failing
 ~~~~~~~
 
-.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @int } }
+.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @integer } }
    :name: fail; gfail
 
    :tacn:`fail` is the always-failing tactic: it does not solve any
@@ -919,7 +919,7 @@ Failing
       the call to :tacn:`fail` :n:`@natural` is not enclosed in a :n:`+` construct,
       respecting the algebraic identity.
 
-   :n:`{* {| @ident | @string | @int } }`
+   :n:`{* {| @ident | @string | @integer } }`
       The given tokens are used for printing the failure message.  If :token:`ident`
       is an |Ltac| variable, its contents are printed; if not, it is an error.
 
@@ -2302,11 +2302,11 @@ performance issue.
 
    This flag enables and disables the profiler.
 
-.. cmd:: Show Ltac Profile {? {| CutOff @int | @string } }
+.. cmd:: Show Ltac Profile {? {| CutOff @integer | @string } }
 
    Prints the profile.
 
-   :n:`CutOff @int`
+   :n:`CutOff @integer`
       By default, tactics that account for less than 2% of the total time are not displayed.
       `CutOff` lets you specify a different percentage.
 
@@ -2373,7 +2373,7 @@ performance issue.
    Equivalent to the :cmd:`Reset Ltac Profile` command, which allows
    resetting the profile from tactic scripts for benchmarking purposes.
 
-.. tacn:: show ltac profile {? {| cutoff @int | @string } }
+.. tacn:: show ltac profile {? {| cutoff @integer | @string } }
    :name: show ltac profile
 
    Equivalent to the :cmd:`Show Ltac Profile` command,
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 9b8749f185..b4f32c6cbb 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -283,7 +283,7 @@ There is dedicated syntax for list and array literals.
    | [ {*; @ltac2_expr5 } ]
    | %{ {? {+ @tac2rec_fieldexpr } {? ; } } %}
    | @ltac2_tactic_atom
-   ltac2_tactic_atom ::= @int
+   ltac2_tactic_atom ::= @integer
    | @string
    | @qualid
    | @ @ident
@@ -1159,7 +1159,7 @@ Match on values
 Notations
 ---------
 
-.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @int } := @ltac2_expr
+.. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @integer } := @ltac2_expr
    :name: Ltac2 Notation
 
    .. todo seems like name maybe should use lident rather than ident, considering:
@@ -1177,7 +1177,7 @@ Notations
 
    :cmd:`Ltac2 Notation` provides a way to extend the syntax of Ltac2 tactics.  The left-hand
    side (before the `:=`) defines the syntax to recognize and gives formal parameter
-   names for the syntactic values.  :n:`@int` is the level of the notation.
+   names for the syntactic values.  :n:`@integer` is the level of the notation.
    When the notation is used, the values are substituted
    into the right-hand side.  The right-hand side is typechecked when the notation is used,
    not when it is defined.  In the following example, `x` is the formal parameter name and
@@ -1333,7 +1333,7 @@ Syntactic classes are described with a form of S-expression:
 
    .. prodn::
       ltac2_scope ::= @string
-      | @int
+      | @integer
       | @name
       | @name ( {+, @ltac2_scope } )
 
@@ -1384,14 +1384,14 @@ table further down lists the classes that that are handled plainly.
   :n:`terminal(@string)`
     Accepts the specified string whether it's a keyword or not, returning a value of `()`.
 
-  :n:`tactic {? (@int) }`
-    Parses an :token:`ltac2_expr`.  If :token:`int` is specified, the construct
-    parses a :n:`ltac2_expr@int`, for example `tactic(5)` parses :token:`ltac2_expr5`.
+  :n:`tactic {? (@integer) }`
+    Parses an :token:`ltac2_expr`.  If :token:`integer` is specified, the construct
+    parses a :n:`ltac2_expr@integer`, for example `tactic(5)` parses :token:`ltac2_expr5`.
     `tactic(6)` parses :token:`ltac2_expr`.
-    :token:`int` must be in the range `0 .. 6`.
+    :token:`integer` must be in the range `0 .. 6`.
 
-    You can also use `tactic` to accept an :token:`int` or a :token:`string`, but there's
-    no syntactic class that accepts *only* an :token:`int` or a :token:`string`.
+    You can also use `tactic` to accept an :token:`integer` or a :token:`string`, but there's
+    no syntactic class that accepts *only* an :token:`integer` or a :token:`string`.
 
     .. todo this doesn't work as expected: "::" is in ltac2_expr1
        Ltac2 Notation "ex4" x(tactic(0)) := x.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 2d1b622a2d..ca50a02562 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -5573,7 +5573,7 @@ Natural number
 
 .. prodn:: nat_or_ident ::= {| @natural | @ident }
 
-where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral
+where :token:`ident` is an Ltac variable denoting a standard |Coq| number
 (should not be the name of a tactic which can be followed by a
 bracket ``[``, like ``do``, ``have``,…)
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index de39edc8e9..2f505e7448 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -1734,7 +1734,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
       followed by destruct applied to the last introduced hypothesis.
 
      .. note::
-        For destruction of a numeral, use syntax :n:`destruct (@natural)` (not
+        For destruction of a number, use syntax :n:`destruct (@natural)` (not
         very interesting anyway).
 
    .. tacv:: destruct @pattern
@@ -1866,7 +1866,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
      introduced hypothesis.
 
      .. note::
-        For simple induction on a numeral, use syntax induction (num)
+        For simple induction on a number, use syntax induction (number)
         (not very interesting anyway).
 
    + In case term is a hypothesis :n:`@ident` of the context, and :n:`@ident`
@@ -2992,7 +2992,7 @@ Performing computations
    | @one_term {? at @occs_nums }
    occs_nums ::= {+ {| @natural | @ident } }
    | - {| @natural | @ident } {* @int_or_var }
-   int_or_var ::= @int
+   int_or_var ::= @integer
    | @ident
    unfold_occ ::= @reference {? at @occs_nums }
    pattern_occ ::= @one_term {? at @occs_nums }
@@ -4737,12 +4737,12 @@ Non-logical tactics
 ------------------------
 
 
-.. tacn:: cycle @int
+.. tacn:: cycle @integer
    :name: cycle
 
-   Reorders the selected goals so that the first :n:`@int` goals appear after the
+   Reorders the selected goals so that the first :n:`@integer` goals appear after the
    other selected goals.
-   If :n:`@int` is negative, it puts the last :n:`@int` goals at the
+   If :n:`@integer` is negative, it puts the last :n:`@integer` goals at the
    beginning of the list.
    The tactic is only useful with a goal selector, most commonly `all:`.
    Note that other selectors reorder goals; `1,3: cycle 1` is not equivalent
@@ -4761,11 +4761,11 @@ Non-logical tactics
       all: cycle 2.
       all: cycle -3.
 
-.. tacn:: swap @int @int
+.. tacn:: swap @integer @integer
    :name: swap
 
    Exchanges the position of the specified goals.
-   Negative values for :n:`@int` indicate counting goals
+   Negative values for :n:`@integer` indicate counting goals
    backward from the end of the list of selected goals. Goals are indexed from 1.
    The tactic is only useful with a goal selector, most commonly `all:`.
    Note that other selectors reorder goals; `1,3: swap 1 3` is not equivalent
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index e13558b440..6c07253bce 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1028,7 +1028,7 @@ described first.
 
    .. prodn::
       strategy_level ::= opaque
-      | @int
+      | @integer
       | expand
       | transparent
       strategy_level_or_var ::= @strategy_level
@@ -1052,7 +1052,7 @@ described first.
 
     + ``opaque`` : level of opaque constants. They cannot be expanded by
       tactics (behaves like +∞, see next item).
-    + :n:`@int` : levels indexed by an integer. Level 0 corresponds to the
+    + :n:`@integer` : levels indexed by an integer. Level 0 corresponds to the
       default behavior, which corresponds to transparent constants. This
       level can also be referred to as ``transparent``. Negative levels
       correspond to constants to be expanded before normal transparent
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 8474d0287f..d31ec51d52 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1887,7 +1887,7 @@ Tactic notations allow customizing the syntax of tactics.
         - :tacn:`refine`
 
       * - ``integer``
-        - :token:`int`
+        - :token:`integer`
         - an integer
         -
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index fbf83760ad..89009764c8 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -736,11 +736,6 @@ export_token: [
 ]
 
 (* lexer stuff *)
-integer: [ | DELETENT ]
-RENAME: [
-| integer int (* todo: review uses in .mlg files, some should be "natural" *)
-]
-
 LEFTQMARK: [
 | "?"
 ]
@@ -766,8 +761,9 @@ natural: [
 | WITH [ decnat | hexnat ]
 ]
 
-int: [
-| OPT "-" natural
+integer: [
+| REPLACE bigint
+| WITH OPT "-" natural
 ]
 
 number: [
@@ -1091,13 +1087,13 @@ simple_tactic: [
 | WITH "subst" OPT ( LIST1 var )
 | DELETE "subst"
 | DELETE "congruence"
-| DELETE "congruence" int
+| DELETE "congruence" integer
 | DELETE "congruence" "with" LIST1 constr
-| REPLACE "congruence" int "with" LIST1 constr
-| WITH "congruence" OPT int OPT ( "with" LIST1 constr )
+| REPLACE "congruence" integer "with" LIST1 constr
+| WITH "congruence" OPT integer OPT ( "with" LIST1 constr )
 | DELETE "show" "ltac" "profile"
-| REPLACE "show" "ltac" "profile" "cutoff" int
-| WITH "show" "ltac" "profile" OPT [ "cutoff" int | string ]
+| REPLACE "show" "ltac" "profile" "cutoff" integer
+| WITH "show" "ltac" "profile" OPT [ "cutoff" integer | string ]
 | DELETE "show" "ltac" "profile" string
 (* perversely, the mlg uses "tactic3" instead of "tactic_expr3" *)
 | DELETE "transparent_abstract" tactic3
@@ -1205,11 +1201,11 @@ command: [
 | REPLACE "Next" "Obligation" "of" ident withtac
 | WITH "Next" "Obligation" OPT ( "of" ident ) withtac
 | DELETE "Next" "Obligation" withtac
-| REPLACE "Obligation" int "of" ident ":" lglob withtac
-| WITH "Obligation" int OPT ( "of" ident ) OPT ( ":" lglob withtac )
-| DELETE "Obligation" int "of" ident withtac
-| DELETE "Obligation" int ":" lglob withtac
-| DELETE "Obligation" int withtac
+| REPLACE "Obligation" integer "of" ident ":" lglob withtac
+| WITH "Obligation" integer OPT ( "of" ident ) OPT ( ":" lglob withtac )
+| DELETE "Obligation" integer "of" ident withtac
+| DELETE "Obligation" integer ":" lglob withtac
+| DELETE "Obligation" integer withtac
 | REPLACE "Obligations" "of" ident
 | WITH "Obligations" OPT ( "of" ident )
 | DELETE "Obligations"
@@ -1229,17 +1225,17 @@ command: [
 | DELETE "Show" ident
 | "Show" OPT [ ident | natural ]
 | DELETE "Show" "Ltac" "Profile"
-| REPLACE "Show" "Ltac" "Profile" "CutOff" int
-| WITH "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ]
+| REPLACE "Show" "Ltac" "Profile" "CutOff" integer
+| WITH "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ]
 | DELETE "Show" "Ltac" "Profile" string
 | DELETE "Show" "Proof"  (* combined with Show Proof Diffs in vernac_toplevel *)
 | REPLACE "Solve" "All" "Obligations" "with" tactic
 | WITH "Solve" "All" "Obligations" OPT ( "with" tactic )
 | DELETE "Solve" "All" "Obligations"
-| REPLACE "Solve" "Obligation" int "of" ident "with" tactic
-| WITH "Solve" "Obligation" int OPT ( "of" ident ) "with" tactic
+| REPLACE "Solve" "Obligation" integer "of" ident "with" tactic
+| WITH "Solve" "Obligation" integer OPT ( "of" ident ) "with" tactic
 | DELETE "Solve" "Obligations"
-| DELETE "Solve" "Obligation" int "with" tactic
+| DELETE "Solve" "Obligation" integer "with" tactic
 | REPLACE "Solve" "Obligations" "of" ident "with" tactic
 | WITH "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" tactic )
 | DELETE "Solve" "Obligations" "with" tactic
@@ -2154,7 +2150,7 @@ tac2expr5: [
 
 RENAME: [
 | Prim.string string
-| Prim.integer int
+| Prim.integer integer
 | Prim.qualid qualid
 | Prim.natural natural
 ]
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 73b721702e..994447b12d 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -598,7 +598,7 @@ command: [
 | "Hint" "Cut" "[" hints_path "]" opthints
 | "Typeclasses" "Transparent" LIST0 reference
 | "Typeclasses" "Opaque" LIST0 reference
-| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT int
+| "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT integer
 | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ]
 | "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ]
 | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic
@@ -652,7 +652,7 @@ command: [
 | "Print" "Rewrite" "HintDb" preident
 | "Reset" "Ltac" "Profile"
 | "Show" "Ltac" "Profile"
-| "Show" "Ltac" "Profile" "CutOff" int
+| "Show" "Ltac" "Profile" "CutOff" integer
 | "Show" "Ltac" "Profile" string
 | "Show" "Lia" "Profile"      (* micromega plugin *)
 | "Add" "Zify" "InjTyp" constr      (* micromega plugin *)
@@ -1715,7 +1715,7 @@ simple_tactic: [
 | "stop" "ltac" "profiling"
 | "reset" "ltac" "profile"
 | "show" "ltac" "profile"
-| "show" "ltac" "profile" "cutoff" int
+| "show" "ltac" "profile" "cutoff" integer
 | "show" "ltac" "profile" string
 | "restart_timer" OPT string
 | "finish_timing" OPT string
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index a021bdbec0..105bd4668e 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -134,7 +134,7 @@ number: [
 | OPT "-" hexnat OPT ( "." LIST1 [ hexdigit | "_" ] ) OPT ( [ "p" | "P" ] OPT [ "+" | "-" ] decnat )
 ]
 
-int: [
+integer: [
 | OPT "-" natural
 ]
 
@@ -514,7 +514,7 @@ occs_nums: [
 ]
 
 int_or_var: [
-| int
+| integer
 | ident
 ]
 
@@ -686,7 +686,7 @@ scope_key: [
 
 strategy_level: [
 | "opaque"
-| int
+| integer
 | "expand"
 | "transparent"
 ]
@@ -827,9 +827,9 @@ command: [
 | "Comments" LIST0 [ one_term | string | natural ]
 | "Declare" "Instance" ident_decl LIST0 binder ":" term OPT hint_info
 | "Declare" "Scope" scope_name
-| "Obligation" int OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
+| "Obligation" integer OPT ( "of" ident ) OPT ( ":" term OPT ( "with" ltac_expr ) )
 | "Next" "Obligation" OPT ( "of" ident ) OPT ( "with" ltac_expr )
-| "Solve" "Obligation" int OPT ( "of" ident ) "with" ltac_expr
+| "Solve" "Obligation" integer OPT ( "of" ident ) "with" ltac_expr
 | "Solve" "Obligations" OPT ( OPT ( "of" ident ) "with" ltac_expr )
 | "Solve" "All" "Obligations" OPT ( "with" ltac_expr )
 | "Admit" "Obligations" OPT ( "of" ident )
@@ -852,7 +852,7 @@ command: [
 | "Optimize" "Proof"
 | "Optimize" "Heap"
 | "Reset" "Ltac" "Profile"
-| "Show" "Ltac" "Profile" OPT [ "CutOff" int | string ]
+| "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ]
 | "Show" "Lia" "Profile"      (* micromega plugin *)
 | "Add" "Zify" "InjTyp" one_term      (* micromega plugin *)
 | "Add" "Zify" "BinOp" one_term      (* micromega plugin *)
@@ -891,7 +891,7 @@ command: [
 | "Hint" "Cut" "[" hints_path "]" OPT ( ":" LIST1 ident )
 | "Typeclasses" "Transparent" LIST0 qualid
 | "Typeclasses" "Opaque" LIST0 qualid
-| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT int
+| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" eauto_search_strategy_name ")" ) OPT integer
 | "Proof" "with" ltac_expr OPT [ "using" section_subset_expr ]
 | "Proof" "using" section_subset_expr OPT [ "with" ltac_expr ]
 | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr
@@ -964,7 +964,7 @@ command: [
 | "Arguments" reference LIST0 arg_specs LIST0 [ "," LIST0 implicits_alt ] OPT [ ":" LIST1 args_modifier SEP "," ]
 | "Implicit" [ "Type" | "Types" ] reserv_list
 | "Generalizable" [ [ "Variable" | "Variables" ] LIST1 ident | "All" "Variables" | "No" "Variables" ]
-| "Set" setting_name OPT [ int | string ]
+| "Set" setting_name OPT [ integer | string ]
 | "Unset" setting_name
 | "Open" "Scope" scope
 | "Close" "Scope" scope
@@ -988,7 +988,7 @@ command: [
 | "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
 | "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
 | "Ltac2" "@" "external" ident ":" ltac2_type ":=" string string
-| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" int ) ":=" ltac2_expr
+| "Ltac2" "Notation" LIST1 ltac2_scope OPT ( ":" integer ) ":=" ltac2_expr
 | "Ltac2" "Set" qualid OPT [ "as" ident ] ":=" ltac2_expr
 | "Ltac2" "Notation" [ string | lident ] ":=" ltac2_expr      (* Ltac2 plugin *)
 | "Ltac2" "Eval" ltac2_expr      (* Ltac2 plugin *)
@@ -1255,7 +1255,7 @@ qhyp: [
 
 int_or_id: [
 | ident
-| int      (* extraction plugin *)
+| integer      (* extraction plugin *)
 ]
 
 language: [
@@ -1417,8 +1417,8 @@ simple_tactic: [
 | "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2
 | "first" "[" LIST0 ltac_expr SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
-| "idtac" LIST0 [ ident | string | int ]
-| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | int ]
+| "idtac" LIST0 [ ident | string | integer ]
+| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | integer ]
 | "fun" LIST1 name "=>" ltac_expr
 | "eval" red_expr "in" term
 | "context" ident "[" term "]"
@@ -1462,7 +1462,7 @@ simple_tactic: [
 | "evar" "(" ident ":" term ")"
 | "evar" one_term
 | "instantiate" "(" ident ":=" term ")"
-| "instantiate" "(" int ":=" term ")" OPT hloc
+| "instantiate" "(" integer ":=" term ")" OPT hloc
 | "instantiate"
 | "stepl" one_term OPT ( "by" ltac_expr )
 | "stepr" one_term OPT ( "by" ltac_expr )
@@ -1501,7 +1501,7 @@ simple_tactic: [
 | "start" "ltac" "profiling"
 | "stop" "ltac" "profiling"
 | "reset" "ltac" "profile"
-| "show" "ltac" "profile" OPT [ "cutoff" int | string ]
+| "show" "ltac" "profile" OPT [ "cutoff" integer | string ]
 | "restart_timer" OPT string
 | "finish_timing" OPT ( "(" string ")" ) OPT string
 | "eassumption"
@@ -1606,7 +1606,7 @@ simple_tactic: [
 | "change_no_check" conversion OPT clause_dft_concl
 | "btauto"
 | "rtauto"
-| "congruence" OPT int OPT ( "with" LIST1 one_term )
+| "congruence" OPT integer OPT ( "with" LIST1 one_term )
 | "f_equal"
 | "firstorder" OPT ltac_expr firstorder_rhs
 | "gintuition" OPT ltac_expr
@@ -2035,7 +2035,7 @@ tac2rec_field: [
 
 ltac2_scope: [
 | string      (* Ltac2 plugin *)
-| int      (* Ltac2 plugin *)
+| integer      (* Ltac2 plugin *)
 | name      (* Ltac2 plugin *)
 | name "(" LIST1 ltac2_scope SEP "," ")"      (* Ltac2 plugin *)
 ]
@@ -2085,7 +2085,7 @@ ltac2_expr0: [
 ]
 
 ltac2_tactic_atom: [
-| int      (* Ltac2 plugin *)
+| integer      (* Ltac2 plugin *)
 | string      (* Ltac2 plugin *)
 | qualid      (* Ltac2 plugin *)
 | "@" ident      (* Ltac2 plugin *)
@@ -2201,7 +2201,7 @@ with_names: [
 ]
 
 occurrences: [
-| LIST1 int
+| LIST1 integer
 | ident
 ]
 
@@ -2296,7 +2296,7 @@ ltac_expr0: [
 ]
 
 tactic_atom: [
-| int
+| integer
 | qualid
 | "()"
 ]
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 35c90444b1..8d197e6056 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -77,7 +77,7 @@ END
 (* true = All transparent, false = Opaque if possible *)
 
 VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> {
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> {
      set_typeclasses_debug d;
      Option.iter set_typeclasses_strategy s;
      set_typeclasses_depth depth
diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg
index eb9d9cbdce..e5309ea441 100644
--- a/plugins/ltac/profile_ltac_tactics.mlg
+++ b/plugins/ltac/profile_ltac_tactics.mlg
@@ -55,7 +55,7 @@ END
 
 TACTIC EXTEND show_ltac_profile
 | [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff }
-| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
+| [ "show" "ltac" "profile" "cutoff" integer(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
 | [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s }
 END
 
@@ -74,7 +74,7 @@ END
 
 VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
 | [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff }
-| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) }
+| [ "Show" "Ltac" "Profile" "CutOff" integer(n) ] -> { print_results ~cutoff:(float_of_int n) }
 END
 
 VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY