Merge PR #13417: Use nat_or_var in grammar where negative values don't make sense

Reviewed-by: Zimmi48

4 files changed, 16 insertions, 14 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index fb9965e43a..28b60878d2 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -250,11 +250,11 @@ proof by abstracting monomials by variables.
 `psatz`: a proof procedure for non-linear arithmetic
 ----------------------------------------------------
 
-.. tacn:: psatz @one_term {? @int_or_var }
+.. tacn:: psatz @one_term {? @nat_or_var }
    :name: psatz
 
    This tactic explores the *Cone* by increasing degrees – hence the
-   depth parameter *n*. In theory, such a proof search is complete – if the
+   depth parameter :token:`nat_or_var`. In theory, such a proof search is complete – if the
    goal is provable the search eventually stops. Unfortunately, the
    external oracle is using numeric (approximate) optimization techniques
    that might miss a refutation.
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index 22527dc379..98445fca1a 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -405,7 +405,7 @@ Summary of the commands
    Shows the list of instances associated with the typeclass :token:`reference`.
 
 
-.. tacn:: typeclasses eauto {? bfs } {? @int_or_var } {? with {+ @ident } }
+.. tacn:: typeclasses eauto {? bfs } {? @nat_or_var } {? with {+ @ident } }
 
    This proof search tactic uses the resolution engine that is run
    implicitly during type checking. This tactic uses a different resolution
@@ -445,11 +445,11 @@ Summary of the commands
    + Use the :cmd:`Typeclasses eauto` command to customize the behavior of
      this tactic.
 
-   :n:`@int_or_var`
+   :n:`@nat_or_var`
      Specifies the maximum depth of the search.
 
       .. warning::
-         The semantics for the limit :n:`@int_or_var`
+         The semantics for the limit :n:`@nat_or_var`
          are different than for :tacn:`auto`. By default, if no limit is given, the
          search is unbounded. Unlike :tacn:`auto`, introduction steps count against
          the limit, which might result in larger limits being necessary when
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 6464f085b8..2fc3c9f748 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -480,15 +480,15 @@ separately.  They succeed only if there is a success for each goal.  For example
 Do loop
 ~~~~~~~
 
-.. tacn:: do @int_or_var @ltac_expr3
+.. tacn:: do @nat_or_var @ltac_expr3
    :name: do
 
-   The do loop repeats a tactic :token:`int_or_var` times:
+   The do loop repeats a tactic :token:`nat_or_var` times:
 
-   :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. This tactic
-   value ``v`` is applied :token:`int_or_var` times. Supposing :token:`int_or_var` > 1, after the
+   :n:`@ltac_expr` is evaluated to ``v``, which must be a tactic value. This tactic
+   value ``v`` is applied :token:`nat_or_var` times. If :token:`nat_or_var` > 1, after the
    first application of ``v``, ``v`` is applied, at least once, to the generated
-   subgoals and so on. It fails if the application of ``v`` fails before :token:`int_or_var`
+   subgoals and so on. It fails if the application of ``v`` fails before :token:`nat_or_var`
    applications have been completed.
 
    :tacn:`do` is an :token:`l3_tactic`.
@@ -973,11 +973,11 @@ Timeout
 We can force a tactic to stop if it has not finished after a certain
 amount of time:
 
-.. tacn:: timeout @int_or_var @ltac_expr3
+.. tacn:: timeout @nat_or_var @ltac_expr3
    :name: timeout
 
    :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value
-   ``v`` is applied normally, except that it is interrupted after :n:`@natural` seconds
+   ``v`` is applied normally, except that it is interrupted after :n:`@nat_or_var` seconds
    if it is still running. In this case the outcome is a failure.
 
    :tacn:`timeout` is an :token:`l3_tactic`.
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 5283f60b11..9ec568c2c7 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -323,10 +323,12 @@ Performing computations
    | delta {? @delta_flag }
    ref_or_pattern_occ ::= @reference {? at @occs_nums }
    | @one_term {? at @occs_nums }
-   occs_nums ::= {+ {| @natural | @ident } }
-   | - {+ {| @natural | @ident } }
+   occs_nums ::= {+ @nat_or_var }
+   | - {+ @nat_or_var }
    int_or_var ::= @integer
    | @ident
+   nat_or_var ::= @natural
+   | @ident
    unfold_occ ::= @reference {? at @occs_nums }
    pattern_occ ::= @one_term {? at @occs_nums }