Merge PR #6708: Mention -quiet flag for Fail

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}