From 0552482c947966f720e265e95db44c45331f38a1 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Thu, 25 Jan 2018 14:31:06 -0500 Subject: document the Fail command --- doc/refman/RefMan-oth.tex | 9 +++++++++ 1 file changed, 9 insertions(+) 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} -- cgit v1.2.3