diff options
author | charguer <arthur@chargueraud.org> | 2018-07-10 16:50:30 +0200 |
---|---|---|
committer | charguer <arthur@chargueraud.org> | 2018-07-10 16:50:30 +0200 |
commit | 3bb14bc0e3665527c8e961b1424df9284c5042b6 (patch) | |
tree | 1f1a769e850352160c502087020fa57dcb737c67 /doc/sphinx/proof-engine | |
parent | 38d4b5cba84a253f2f4ea4febda9f60fde2052c9 (diff) |
fixed typo for assert_suceed
Diffstat (limited to 'doc/sphinx/proof-engine')
-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`. |