From 70b18cd58243c99b13eefbd9c593b0f3929c742c Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Tue, 24 Nov 2020 15:09:28 -0800
Subject: Use nat_or_var for fail/gfail

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

(limited to 'doc/sphinx')

diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 8b627c29a4..013ff0a83f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -879,7 +879,7 @@ Print/identity tactic: idtac
 Failing
 ~~~~~~~
 
-.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @natural } }
+.. tacn:: {| fail | gfail } {? @nat_or_var } {* {| @ident | @string | @natural } }
    :name: fail; gfail
 
    :tacn:`fail` is the always-failing tactic: it does not solve any
@@ -900,7 +900,7 @@ Failing
    tactic into the goals, meaning that if there are no goals when it is
    evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed.
 
-   :n:`@int_or_var`
+   :n:`@nat_or_var`
       The failure level. If no level is specified, it defaults to 0.
       The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching
       tacticals. If 0, it makes :tacn:`match goal` consider the next clause
-- 
cgit v1.2.3