aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 15:09:30 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-09 15:09:30 +0100
commitd04f262f4c27a086b9ddfef1931586ef1062614d (patch)
tree14c13f9879e6c92561627e6308ba6801ea2ed2b6 /doc
parent2069c0aec44a50031e33bcb9f7d86c1535ef6b84 (diff)
parentaa95d82692684a416d7a1c25fce38b4eca1e49c9 (diff)
Merge PR #6820: Tacticals assert_fails and assert_succeeds
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-ltac.tex18
1 files changed, 18 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 0a4d0ef9a..3ed697d8b 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -156,6 +156,8 @@ is understood as
& | & {\tt type\_term} {\term}\\
& | & {\tt numgoals} \\
& | & {\tt guard} {\it test}\\
+& | & {\tt assert\_fails} {\tacexprpref}\\
+& | & {\tt assert\_succeds} {\tacexprpref}\\
& | & \atomictac\\
& | & {\qualid} \nelist{\tacarg}{}\\
& | & {\atom}
@@ -598,6 +600,22 @@ The experimental status of this tactic pertains to the fact if $v$ performs side
\ErrMsg \errindex{This tactic has more than one success}
+\subsubsection[Checking the failure]{Checking the failure\tacindex{assert\_fails}\index{Tacticals!assert\_fails@{\tt assert\_fails}}}
+
+Coq provides a derived tactic to check that a tactic \emph{fails}:
+\begin{quote}
+{\tt assert\_fails} {\tacexpr}
+\end{quote}
+This behaves like {\tt tryif {\tacexpr} then fail 0 tac "succeeds" else idtac}.
+
+\subsubsection[Checking the success]{Checking the success\tacindex{assert\_succeeds}\index{Tacticals!assert\_succeeds@{\tt assert\_succeeds}}}
+
+Coq provides a derived tactic to check that a tactic has \emph{at least one} success:
+\begin{quote}
+{\tt assert\_succeeds} {\tacexpr}
+\end{quote}
+This behaves like {\tt tryif (assert\_fails tac) then fail 0 tac "fails" else idtac}.
+
\subsubsection[Solving]{Solving\tacindex{solve}
\index{Tacticals!solve@{\tt solve}}}