From 7ca4cd26d67070058589031b693454cd2858e4e9 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Wed, 16 Aug 2017 16:32:44 +0200
Subject: Adding documentation for Printing Focused option.

---
 doc/refman/RefMan-oth.tex | 15 ++++++++++++++-
 doc/refman/RefMan-pro.tex |  4 ++--
 2 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index bf48057cdf..8f43ebcfbc 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -974,7 +974,20 @@ line provided it does not exceed the printing width (See {\tt Set
   Printing Width} above).
 
 \subsection[\tt Test Printing Compact Contexts.]{\tt Test Printing Compact Contexts.\optindex{Printing Compact Contexts}}
-This command displays the current state of compaction of goal d'isolat.
+This command displays the current state of compaction of goal.
+
+
+\subsection[\tt Unset Printing Unfocused.]{\tt Unset Printing Unfocused.\optindex{Printing Unfocused}}
+This command resets the displaying of goals to focused goals only
+(default). Unfocused goals are created by focusing other goals with
+bullets(see~\ref{bullets}) or curly braces (see~\ref{curlybacket}).
+
+\subsection[\tt Set Printing Unfocused.]{\tt Set Printing Unfocused.\optindex{Printing Unfocused}}
+This command enables the displaying of unfocused goals. The goals are
+displayed after the focused ones and are distinguished by a separator.
+
+\subsection[\tt Test Printing Unfocused.]{\tt Test Printing Unfocused.\optindex{Printing Unfocused}}
+This command displays the current state of unfocused goals display.
 
 \subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}}
 This command enables the printing of the ``{\tt (dependent evars: \ldots)}''
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 95fee3241c..eb59ca584e 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -308,7 +308,7 @@ last {\tt Focus} command.
 Succeeds in the proof is fully unfocused, fails is there are some
 goals out of focus.
 
-\subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}
+\subsection[\tt \{ \textrm{and} \}]{\tt \{ \textrm{and} \}\comindex{\{}\comindex{\}}}\label{curlybacket}
 The command {\tt \{} (without a terminating period) focuses on the
 first goal, much like {\tt Focus.} does, however, the subproof can
 only be unfocused when it has been fully solved (\emph{i.e.} when
@@ -327,7 +327,7 @@ unfocus it or focus the next one.
 \end{ErrMsgs}
 
 \subsection[Bullets]{Bullets\comindex{+ (command)}
-  \comindex{- (command)}\comindex{* (command)}\index{Bullets}}
+  \comindex{- (command)}\comindex{* (command)}\index{Bullets}}\label{bullets}
 Alternatively to {\tt \{} and {\tt \}}, proofs can be structured with
 bullets. The use of a bullet $b$ for the first time focuses on the
 first goal $g$, the same bullet cannot be used again until the proof
-- 
cgit v1.2.3