From 3bb14bc0e3665527c8e961b1424df9284c5042b6 Mon Sep 17 00:00:00 2001 From: charguer Date: Tue, 10 Jul 2018 16:50:30 +0200 Subject: fixed typo for assert_suceed --- doc/sphinx/proof-engine/ltac.rst | 4 ++-- 1 file 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`. -- cgit v1.2.3