3 files changed, 19 insertions, 14 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
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 084317776b..d8a353300f 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -980,7 +980,7 @@ delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope}
 
 This scope includes the standard arithmetical operators and relations on
 type {\tt N} (binary natural numbers). It is delimited by key {\tt N}
-and comes with an interpretation for numerals as closed term of type {\tt Z}.
+and comes with an interpretation for numerals as closed term of type {\tt N}.
 
 \subsubsection{\tt Z\_scope}
 
@@ -1014,16 +1014,8 @@ fractions of an integer and a strictly positive integer.
 
 This scope includes the standard arithmetical operators and relations on
 type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R}
-and comes with an interpretation for numerals as term of type {\tt
-R}. The interpretation is based on the binary decomposition.  The
-numeral 2 is represented by $1+1$.  The interpretation $\phi(n)$ of an
-odd positive numerals greater $n$ than 3 is {\tt 1+(1+1)*$\phi((n-1)/2)$}.
-The interpretation $\phi(n)$ of an even positive numerals greater $n$
-than 4 is {\tt (1+1)*$\phi(n/2)$}.  Negative numerals are represented as the
-opposite of the interpretation of their absolute value. E.g. the
-syntactic object {\tt -11} is interpreted as {\tt
--(1+(1+1)*((1+1)*(1+(1+1))))} where the unit $1$ and all the operations are
-those of {\tt R}.
+and comes with an interpretation for numerals using the {\tt IZR}
+morphism from binary integer numbers to {\tt R}.
 
 \subsubsection{\tt bool\_scope}