Doc for Combined Scheme.

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

1 files changed, 18 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index a29dcbfd8..f62412f8f 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3323,6 +3323,24 @@ general principle of mutual induction for objects in type {\term$_i$}.
 
 \SeeAlso Section~\ref{Scheme-examples}
 
+\subsection{\tt Combined Scheme\label{CombinedScheme}
+\comindex{Combined Scheme}}
+The {\tt Combined Scheme} command is a tool for combining 
+induction principles generated by the {\tt Scheme} command.
+Its syntax follows the schema :
+
+\noindent
+{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}\\
+\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
+the same package of mutual inductive principle definitions. This command
+generates {\ident$_0$} to be the conjunction of the principles: it is
+built from the common premises of the principles and concluded by the
+conjunction of their conclusions.
+
+\SeeAlso \ref{CombinedScheme-examples}
+
+\SeeAlso Section~\ref{CombinedScheme-examples}
+
 \section{Generation of induction principles with {\tt Functional Scheme}
 \label{FunScheme}
 \comindex{Functional Scheme}}