diff options
| author | Jim Fehrle | 2020-11-24 15:09:28 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2021-01-07 13:50:58 -0800 |
| commit | 70b18cd58243c99b13eefbd9c593b0f3929c742c (patch) | |
| tree | ecef0a61d175c31a7852034d0fa727cc6891e9f0 /doc/sphinx | |
| parent | 7b946aa196490be8790cd5b46d0860b3bf6e33e1 (diff) | |
Use nat_or_var for fail/gfail
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 4 |
1 files changed, 2 insertions, 2 deletions
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 |