3 files changed, 60 insertions, 4 deletions
diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex
index 3389382af..52935b93c 100644
--- a/doc/refman/RefMan-ind.tex
+++ b/doc/refman/RefMan-ind.tex
@@ -468,9 +468,9 @@ natural in case of inductively defined relations.
 
 \Example
 With the predicates {\tt odd} and {\tt even} inductively defined as:
-\begin{coq_eval}
-Restore State "Initial".
-\end{coq_eval}
+% \begin{coq_eval}
+% Restore State "Initial".
+% \end{coq_eval}
 \begin{coq_example*}
 Inductive odd : nat -> Prop :=
     oddS : forall n:nat, even n -> odd (S n)
@@ -491,7 +491,25 @@ Check odd_even.
 The type of {\tt even\_odd} shares the same premises but the
 conclusion is {\tt (n:nat)(even n)->(Q n)}.
 
+\subsection{\tt Combined Scheme ...}\index{CombinedScheme@{\tt Combined Scheme}}\label{CombinedScheme}
+\label{combinedscheme}
+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
+build from the common premises of the principles and concluded by the
+conjunction of their conclusions. For exemple, we can combine the
+induction principles for trees and forests:
+
+\begin{coq_example*}
+Mutual Scheme tree_forest_mutind from tree_ind, forest_ind.
+Check tree_forest_mutind.
+\end{coq_example*}
 
 %\end{document}
 
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}}
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 0aee43178..8cb7a4807 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -241,8 +241,8 @@ Check forest_tree_rec.
 
 Let {\tt odd} and {\tt even} be inductively defined as:
 
+% Reset Initial.
 \begin{coq_eval}
-Reset Initial.
 Open Scope nat_scope.
 \end{coq_eval}
 
@@ -271,6 +271,26 @@ Check odd_even.
 The type of {\tt even\_odd} shares the same premises but the
 conclusion is {\tt (n:nat)(even n)->(Q n)}.
 
+\subsection{{\tt Combined Scheme}}
+\comindex{Combined Scheme}
+\label{CombinedScheme-examples}
+
+We can define the induction principles for trees and forests using:
+\begin{coq_example}
+Scheme tree_forest_ind := Induction for tree Sort Prop
+  with forest_tree_ind := Induction for forest Sort Prop.
+\end{coq_example}
+
+Then we can build the combined induction principle:
+\begin{coq_example}
+Combined Scheme tree_forest_mutind from tree_forest_ind, forest_tree_ind.
+\end{coq_example}
+
+The type of {\tt tree\_forest\_mutrec} will be:
+\begin{coq_example}
+Check tree_forest_mutind.
+\end{coq_example}
+
 \section{{\tt Functional Scheme} and {\tt functional induction}}
 \comindex{Functional Scheme}\tacindex{functional induction}
 \label{FunScheme-examples}