From e74d328b32634a44ab049f971ec33fe6cd24df72 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 18 Nov 2020 13:18:04 -0800
Subject: Use nat_or_var where negative values don't make sense

---
 doc/sphinx/proof-engine/ltac.rst | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'doc/sphinx/proof-engine')

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`.
-- 
cgit v1.2.3