diff options
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 3ebeba178..65926c69c 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -912,6 +912,15 @@ This command turns off the use of a default timeout. This command displays whether some default timeout has be set or not. +\subsection[\tt Fail \textrm{\textsl{command-or-tactic}}.]{\tt Fail \textrm{\textsl{command-or-tactic}}.\comindex{Fail}\label{Fail}} + +For debugging {\Coq} scripts, sometimes it is desirable to know +whether a command or a tactic fails. If the given command or tactic +fails, the {\tt Fail} statement succeeds, without changing the proof +state, and {\Coq} prints a message confirming the failure. If the +command or tactic succeeds, the statement is an error, and {\Coq} +prints a message indicating that the failure did not occur. + \section{Controlling display} \subsection[\tt Set Silent.]{\tt Set Silent.\optindex{Silent} |