Typos, ajout Set Printing All

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8548 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 34 insertions, 6 deletions

diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index 192e1f2dc..f52e1cf2e 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -995,8 +995,8 @@ To display the implicit arguments associated to an object use command
 \end{quote}
 
 \subsection{Explicitation of implicit arguments for pretty-printing
-\comindex{Set Print Implicit}
-\comindex{Unset Print Implicit}}
+\comindex{Set Printing Implicit}
+\comindex{Unset Printing Implicit}}
 
 By default the basic pretty-printing rules hide the inferable implicit
 arguments of an application. To force printing all implicit arguments,
@@ -1009,6 +1009,8 @@ Conversely, to restore the hidding of implicit arguments, use command
 {\tt Unset Printing Implicit.}
 \end{quote}
 
+\SeeAlso {\tt Set Printing All} in section \ref{SetPrintingAll}.
+
 \subsection{Canonical structures
 \comindex{Canonical Structure}}
 
@@ -1122,6 +1124,30 @@ coercion between {\class$_1$} and {\class$_2$}.
 More details and examples, and a description of the commands related
 to coercions are provided in chapter \ref{Coercions-full}.
 
+\section{Printing constructions in full}
+\label{SetPrintingAll}
+\comindex{Set Printing All}
+\comindex{Unset Printing All}
+
+Coercions, implicit arguments, the type of pattern-matching, but also
+notations (see chapter \ref{Addoc-syntax}) can obfuscate the behavior
+of some tactics (typically the tactics applying to occurrences of
+subterms are sensitive to the implicit arguments). The command
+\begin{quote}
+{\tt Set Printing All.}
+\end{quote}
+deactivates all high-level printing features such as coercions,
+implicit arguments, returned type of pattern-matching, notations and
+various syntactic sugar for pattern-matching or record projections.
+Otherwise said, {\tt Set Printing All} includes the effects
+of the commands {\tt Set Printing Implicit}, {\tt Set Printing
+Coercions}, {\tt Set Printing Synth}, {\tt Unset Printing Projections}
+and {\tt Unset Printing Notations}.  To reactivate the high-level
+printing features, use the command
+\begin{quote}
+{\tt Unset Printing All.}
+\end{quote}
+
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index 3fffcdf21..e15935ece 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -400,19 +400,21 @@ where "n + m" := (plus n m).
 \end{coq_example*}
 
 \subsection{Displaying informations about notations
-\comindex{Set Printing Notation}
-\comindex{Unset Printing Notation}}
+\comindex{Set Printing Notations}
+\comindex{Unset Printing Notations}}
 
 To deactivate the printing of all notations, use the command
 \begin{quote}
-\tt Unset Printing Notation.
+\tt Unset Printing Notations.
 \end{quote}
 To reactivate it, use the command
 \begin{quote}
-\tt Set Printing Notation.
+\tt Set Printing Notations.
 \end{quote}
 The default is to use notations for printing terms wherever possible.
 
+\SeeAlso {\tt Set Printing All} in section \ref{SetPrintingAll}.
+
 \subsection{Locating notations
 \comindex{Locate}
 \label{LocateSymbol}}