From 699d958ec4113094bd690bd3361af7c66e8ee482 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Wed, 7 Feb 2018 13:34:06 -0500
Subject: mention interactive mode for Fail message

---
 doc/refman/RefMan-oth.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

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}
 
-- 
cgit v1.2.3