Ajout intro-pattern des inductifs unaire

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

1 files changed, 8 insertions, 3 deletions

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 3d09c12490..297d10035b 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -982,8 +982,9 @@ induction n.
   \ref{intros-pattern}). This provides a concise notation for nested
   induction.
 
-  It is recommended to use this variant of {\tt induction} for 
-  robust proof scripts.
+\Rem for an inductive type with one constructeur, the pattern notation
+{\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
+{\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}.
 
 \item {\tt induction {\term} using {\qualid}}
 
@@ -1124,6 +1125,10 @@ last introduced hypothesis.
 %  It is recommended to use this variant of {\tt destruct} for 
 %  robust proof scripts.
 
+\Rem for an inductive type with one constructeur, the pattern notation
+{\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
+{\tt [} $p_{1} $\ldots $p_{n}$ {\tt ]}.
+
 \item{\tt destruct {\term} using {\qualid}}
 
   This is a synonym of {\tt induction {\term} using {\qualid}}.
@@ -2428,7 +2433,7 @@ main subgoal excluded.
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_AutoRewrite.v}
 
-\section{The hints databases for auto and eauto}
+\section{The hints databases for {\tt auto} and {\tt eauto}ê}
 \index{Hints databases}\label{Hints-databases}\comindex{Hint}
 The hints for \texttt{auto} and \texttt{eauto} are stored in databases.
 Each databases maps head