Documentation Declare Implicit Tactic, Print Canonical Projections, ... + légère restructuration autour de Proof with et Hint Rewrite + maj crédits

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

1 files changed, 12 insertions, 0 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 73fb391ddb..37660aa3a7 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1118,6 +1118,18 @@ the declaration
 \SeeAlso more examples in user contribution \texttt{category}
 (\texttt{Rocq/ALGEBRA}).
 
+\subsubsection{Print Canonical Projections.
+\comindex{Print Canonical Projections}}
+
+This displays the list of global names that are components of some
+canonical structure. For each of them, the canonical structure of
+which it is a projection is indicated. For instance, the above example 
+gives the following output:
+
+\begin{coq_example}
+Print Canonical Projections.
+\end{coq_example}
+
 \subsection{Implicit types of variables}
 
 It is possible to bind variable names to a given type (e.g. in a