Changements sur Functional xxx. Plus précis et plus exact.

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

1 files changed, 13 insertions, 2 deletions

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index be80e7eb7..584485108 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1349,8 +1349,8 @@ not work for non structural recursive functions. % VRAI??
 
 See the documentation of {\tt functional induction} (section
 \ref{FunInduction}) and {\tt Functional Scheme} (section
-\ref{FunScheme-examples}) for how to use the induction principle to
-easily reason about the function.
+\ref{FunScheme} and \ref{FunScheme-examples}) for how to use the 
+induction principle to easily reason about the function.
 
 \noindent {\bf Remark: } To obtain the right principle, it is better
 to put rigid parameters of the function as first arguments. For
@@ -1382,6 +1382,17 @@ Function plus (n m : nat) {struct n} : nat :=
 \emph{at the end} of each branch.  For now dependent cases are not
 treated.
 
+\paragraph{Difference with \texttt{Functional Scheme}} 
+There is a difference between obtaining an induction scheme for a
+function by using the \texttt{Function} (section~\ref{Function}) and
+by using Functional Scheme after a normal definition using
+\texttt{Fixpoint} or \texttt{Definition}. Indeed \texttt{Function}
+generally produces smaller principles, closer to the definition
+written by the user. This is because \texttt{Functional Scheme} works
+by analyzing the term \texttt{div2} after the compilation of pattern
+matching into exhaustive expanded ones, whereas \texttt{Function}
+analyzes the pseudo-term \emph{before} pattern matching expansion.
+
 
 \ErrMsg