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 | |
| parent | 38d4b5cba84a253f2f4ea4febda9f60fde2052c9 (diff) | |
fixed typo for assert_suceed
| -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`. |