From f8748c9ba3b96d3a9380a6f93c4bf1ca9dc4920c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 15 Oct 2004 16:53:29 +0000
Subject: Documentation 'Focus num'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8590 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-pro.tex | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

(limited to 'doc')

diff --git a/doc/RefMan-pro.tex b/doc/RefMan-pro.tex
index 1411d9afb7..68f96f7cca 100755
--- a/doc/RefMan-pro.tex
+++ b/doc/RefMan-pro.tex
@@ -280,10 +280,16 @@ This command restores the proof editing process to the original goal.
 \end{ErrMsgs}
 
 \subsection{\tt Focus.}\comindex{Focus}
-Will focus the attention on the first subgoal to prove, the remaining
-subgoals will no more be printed after the application of a tactic.
-This is useful when there are many current subgoals which clutter your
-screen.
+This focuses the attention on the first subgoal to prove and the printing
+of the other subgoals is suspended until the focused subgoal is
+solved or unfocused. This is useful when there are many current
+subgoals which clutter your screen.
+
+\begin{Variant}
+\item {\tt Focus {\num}.}\\ 
+This focuses the attention on the $\num^{\scriptsize th}$ subgoal to prove.
+
+\end{Variant}
 
 \subsection{\tt Unfocus.}\comindex{Unfocus}
 Turns off the focus mode.
-- 
cgit v1.2.3