diff options
| -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 88c1e225f..278a4ff01 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -117,7 +117,7 @@ mode but it can also be used in toplevel definitions as shown below. : | numgoals : | guard `test` : | assert_fails `tacexpr3` - : | assert_suceeds `tacexpr3` + : | assert_succeeds `tacexpr3` : | `atomic_tactic` : | `qualid` `tacarg` ... `tacarg` : | `atom` @@ -500,7 +500,7 @@ Coq provides a derived tactic to check that a tactic has *at least one* success: .. tacn:: assert_succeeds @expr - :name: assert_suceeds + :name: assert_succeeds This behaves like :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`. |