Update documentation on tokens, use "int" and "num"

for integers and natural nums

2 files changed, 13 insertions, 13 deletions

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 46f9826e41..362c3da6cb 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -31,10 +31,10 @@ Syntax
 The syntax of the tactic language is given below. See Chapter
 :ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used
 in these grammar rules. Various already defined entries will be used in this
-chapter: entries :token:`natural`, :token:`integer`, :token:`ident`,
+chapter: entries :token:`num`, :token:`int`, :token:`ident`
 :token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic`
-represent respectively the natural and integer numbers, the authorized
-identificators and qualified names, Coq terms and patterns and all the atomic
+represent respectively natural and integer numbers,
+identifiers, qualified names, Coq terms, patterns and the atomic
 tactics described in Chapter :ref:`tactics`.
 
 The syntax of :production:`cpattern` is
@@ -141,10 +141,10 @@ mode but it can also be used in toplevel definitions as shown below.
                      : `atom`
    atom              : `qualid`
                      : ()
-                     : `integer`
+                     : `int`
                      : ( `ltac_expr` )
    component : `string` | `qualid`
-   message_token     : `string` | `ident` | `integer`
+   message_token     : `string` | `ident` | `int`
    tacarg            : `qualid`
                      : ()
                      : ltac : `atom`
@@ -159,11 +159,11 @@ mode but it can also be used in toplevel definitions as shown below.
    match_rule        : `cpattern` => `ltac_expr`
                      : context [`ident`] [ `cpattern` ] => `ltac_expr`
                      : _ => `ltac_expr`
-   test              : `integer` = `integer`
-                     : `integer` (< | <= | > | >=) `integer`
+   test              : `int` = `int`
+                     : `int` (< | <= | > | >=) `int`
    selector          : [`ident`]
-                     : `integer`
-                     : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`)
+                     : `int`
+                     : (`int` | `int` - `int`), ..., (`int` | `int` - `int`)
    toplevel_selector : `selector`
                      : all
                      : par
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 3036648b08..ceaa2775bf 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -179,7 +179,7 @@ constructions from ML.
                     : let `ltac2_var` := `ltac2_term` in `ltac2_term`
                     : let rec `ltac2_var` := `ltac2_term` in `ltac2_term`
                     : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end
-                    : `integer`
+                    : `int`
                     : `string`
                     : `ltac2_term` ; `ltac2_term`
                     : [| `ltac2_term` ; ... ; `ltac2_term` |]
@@ -670,7 +670,7 @@ A scope is a name given to a grammar entry used to produce some Ltac2 expression
 at parsing time. Scopes are described using a form of S-expression.
 
 .. prodn::
-   ltac2_scope ::= {| @string | @integer | @lident ({+, @ltac2_scope}) }
+   ltac2_scope ::= {| @string | @int | @lident ({+, @ltac2_scope}) }
 
 A few scopes contain antiquotation features. For sake of uniformity, all
 antiquotations are introduced by the syntax :n:`$@lident`.
@@ -719,7 +719,7 @@ The following scopes are built-in.
 
   + parses a Ltac2 expression at the next level and return it as is.
 
-- :n:`tactic(n = @integer)`:
+- :n:`tactic(n = @int)`:
 
   + parses a Ltac2 expression at the provided level :n:`n` and return it as is.
 
@@ -760,7 +760,7 @@ Notations
 
 The Ltac2 parser can be extended by syntactic notations.
 
-.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @integer} := @ltac2_term
+.. cmd:: Ltac2 Notation {+ {| @lident (@ltac2_scope) | @string } } {? : @int} := @ltac2_term
    :name: Ltac2 Notation
 
    A Ltac2 notation adds a parsing rule to the Ltac2 grammar, which is expanded