diff options
Diffstat (limited to 'doc/refman/RefMan-gal.tex')
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 5844851081..a145c440de 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -1384,8 +1384,8 @@ 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 +function by using \texttt{Function} (section~\ref{Function}) and +by using \texttt{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 |