diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-07 08:39:02 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-06-07 08:39:02 +0000 |
| commit | 25733d558457c62b01e3ba206f9d24a7fe5dacb9 (patch) | |
| tree | 4cff4e17445405408db9338d3f43689c97d7a282 | |
| parent | 658694c4ccd9abb9e5fa52e72c2a0e3c07490b1e (diff) | |
mise en texttt d'une commande.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8909 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 584485108..a145c440d 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 |