diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-11 12:58:30 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-11 12:58:30 +0200 |
| commit | b646ab446866160b3c657f0134e93fdf002cbc7f (patch) | |
| tree | 616a864eb04c9c23ccf1c43697b3b22d79ea62cb | |
| parent | 79b2f30b22e1a0baeea614813e6984871ec16089 (diff) | |
| parent | 3bb14bc0e3665527c8e961b1424df9284c5042b6 (diff) | |
Merge PR #8035: Fix #8033: Tactic assert-suceeds has a typo in its name in the manual
| -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`. |