[refman] Rename int to integer

5 files changed, 29 insertions, 29 deletions

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