1 files changed, 72 insertions, 20 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 72df6005..f034df41 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1015,7 +1015,7 @@ equivalent to {\tt intros; apply ci}.
 \end{Variants}
 
 \section{Eliminations (Induction and Case Analysis)}
-
+\label{Tac-induction}
 Elimination tactics are useful to prove statements by induction or
 case analysis.  Indeed, they make use of the elimination (or
 induction) principles generated with inductive definitions (see
@@ -1387,42 +1387,83 @@ Qed.
 \end{Variants}
 
 
-\subsection{\tt functional induction \ident\ \term$_1$ \dots\ \term$_n$.
+\subsection{\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$).
 \tacindex{functional induction}
 \label{FunInduction}}
 
-The \emph{experimental} tactic \texttt{functional induction}
-performs case analysis and induction following the definition of
-a (not mutually recursive) function.
+The \emph{experimental} tactic \texttt{functional induction} performs
+case analysis and induction following the definition of a function. It
+makes use of a principle generated by \texttt{Function}
+(section~\ref{Function}) or \texttt{Functional Scheme}
+(section~\ref{FunScheme}). This principle is named \ident\_ind by
+default but you can give it explicitly, see variants below.
 
 \begin{coq_eval}
 Reset Initial.
 \end{coq_eval}
 \begin{coq_example}
+Functional Scheme minus_ind := Induction for minus Sort Prop.
+
 Lemma le_minus : forall n m:nat, (n - m <= n).
 intros n m.
-functional induction minus n m; simpl; auto.
+functional induction (minus n m); simpl; auto.
 \end{coq_example}
 \begin{coq_example*}
 Qed.
 \end{coq_example*}
 
-\texttt{functional induction} is a shorthand for the more general
-command \texttt{Functional Scheme} which builds induction
-principles following the recursive structure of (possibly
-mutually recursive)
-functions. \SeeAlso{\ref{FunScheme-examples}} for the difference
-between using one or the other.
+\Rem \texttt{(\ident\ \term$_1$ \dots\ \term$_n$)} must be a correct
+full application of \ident. In particular, the rules for implicit
+arguments are the same as usual. For example use \texttt{@\ident} if
+you want to write implicit arguments explicitly.
+
+\Rem Parenthesis over \ident \dots \term$_n$ are not mandatory, but if
+there are not written then implicit arguments must be given.
+
+\Rem \texttt{functional induction (f x1 x2 x3)} is actually a
+shorthand for \texttt{induction x1 x2 x3 (f x1 x2 x3) using f\_ind}.
+\texttt{f\_ind} being an induction scheme computed by the
+\texttt{Function} (section~\ref{Function}) or \texttt{Functional
+  Scheme} (section~\ref{FunScheme}) command . Therefore
+\texttt{functional induction} may fail if the induction scheme
+(\texttt{f\_ind}) is not defined. See also section~\ref{Function} for
+the function terms accepted by \texttt{Function}.
+
+\Rem There is a difference between obtaining an induction scheme for a
+function by using \texttt{Function} (section~\ref{Function}) and by
+using \texttt{Functional Scheme} after a normal definition using
+\texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for
+details.
+
+\SeeAlso{\ref{Function},\ref{FunScheme},\ref{FunScheme-examples}}
+
+\ErrMsg 
+
+\errindex{The reference \ident\_ind was not found in the current
+environment}
+
+~
 
-\Rem \texttt{functional induction} may fail on functions built by
-tactics. In particular case analysis of a function are considered
-only if they are not inside an application.
+\errindex{Not the right number of induction arguments}
+ 
+
+\begin{Variants}
+\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
+   using \term$_{m+1}$ with {\term$_{n+1}$} \dots {\term$_m$}}
 
-\Rem Arguments of the function must be given, including the
-implicit ones. If the function is recursive, arguments must be
-variables, otherwise they may be any term.
+ Similar to \texttt{Induction} and \texttt{elim}
+ (section~\ref{Tac-induction}), allows to give explicitly the
+ induction principle and the values of dependent premises of the
+ elimination scheme, including \emph{predicates} for mutual induction
+ when \ident is mutually recursive.
 
-\SeeAlso{\ref{FunScheme},\ref{FunScheme-examples}}
+\item {\tt functional induction (\ident\ \term$_1$ \dots\ \term$_n$)
+    using \term$_{m+1}$ with {\vref$_1$} := {\term$_{n+1}$} \dots\
+    {\vref$_m$} := {\term$_n$}}
+
+  Similar to \texttt{induction} and \texttt{elim}
+  (section~\ref{Tac-induction}).
+\end{Variants}
 
 \section{Equality}
 
@@ -2067,6 +2108,17 @@ datatype: see~\ref{quote-examples} for the full details.
 % En attente d'un moyen de valoriser les fichiers de demos
 % \SeeAlso file \texttt{theories/DEMOS/DemoQuote.v} in the distribution
 
+\section{Classical tactics}
+\label{ClassicalTactics}
+
+In order to ease the proving process, when the {\tt Classical} module is loaded. A few more tactics are available. Make sure to load the module using the \texttt{Require Import} command.
+
+\subsection{{\tt classical\_left, classical\_right} \tacindex{classical\_left} \tacindex{classical\_right}}
+
+The tactics \texttt{classical\_left} and \texttt{classical\_right} are the analog of the \texttt{left} and \texttt{right} but using classical logic. They can only be used for disjunctions.
+Use  \texttt{classical\_left} to prove the left part of the disjunction with the assumption that the negation of right part holds. 
+Use \texttt{classical\_left} to prove the right part of the disjunction with the assumption that the negation of left part holds. 
+
 \section{Automatizing
 \label{Automatizing}}
 
@@ -3087,7 +3139,7 @@ The chapter~\ref{TacticLanguage} gives examples of more complex
 user-defined tactics.
 
 
-% $Id: RefMan-tac.tex 8606 2006-02-23 13:58:10Z herbelin $ 
+% $Id: RefMan-tac.tex 8938 2006-06-09 16:29:01Z jnarboux $ 
 
 %%% Local Variables: 
 %%% mode: latex