diff options
author | Paul Steckler <steck@stecksoft.com> | 2018-02-07 13:34:06 -0500 |
---|---|---|
committer | Paul Steckler <steck@stecksoft.com> | 2018-02-07 13:34:06 -0500 |
commit | 699d958ec4113094bd690bd3361af7c66e8ee482 (patch) | |
tree | 9aade2ad452e7aee0bd10a721c4b50458f98847a /doc | |
parent | 47e43e229ab02a4dedc2405fed3960a4bf476b58 (diff) |
mention interactive mode for Fail message
Diffstat (limited to 'doc')
-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 65926c69c..1cd23c929 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} |