From 25733d558457c62b01e3ba206f9d24a7fe5dacb9 Mon Sep 17 00:00:00 2001
From: courtieu
Date: Wed, 7 Jun 2006 08:39:02 +0000
Subject: mise en texttt d'une commande.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8909 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-gal.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

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
-- 
cgit v1.2.3