diff options
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 65926c69c0..1cd23c9297 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -917,9 +917,9 @@ This command displays whether some default timeout has be set or not. 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. +state, and in interactive mode, {\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} |