From 8a8a4ebc7a416a2d908cdb07c0036e5eefa88d4e Mon Sep 17 00:00:00 2001
From: courtieu
Date: Wed, 7 Jun 2006 15:17:13 +0000
Subject: petites corrections dans la doc de functional xxx.

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

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index a145c440de..c2869fd3da 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1378,14 +1378,14 @@ Function plus (n m : nat) {struct n} : nat :=
 \paragraph{Limitations}
 \label{sec:Function-limitations}
 \term$_0$ must be build as a \emph{pure pattern-matching tree}
-(\texttt{match...with}) with $\lambda$-abstraction and applications only
+(\texttt{match...with}) with $\lambda$-abstractions and applications only
 \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 \texttt{Function} (section~\ref{Function}) and
-by using \texttt{Functional Scheme} after a normal definition using
+by using \texttt{Functional Scheme} after a usual 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
@@ -1399,8 +1399,8 @@ analyzes the pseudo-term \emph{before} pattern matching expansion.
 \errindex{while trying to define Inductive R\_\ident ...}
 
 The generation of the graph relation \texttt{(R\_\ident)} used to
-compute the induction scheme of \ident raised a typing error, the
-definition of \ident was aborted. You can use \texttt{Fixpoint}
+compute the induction scheme of \ident\ raised a typing error, the
+definition of \ident\ was aborted. You can use \texttt{Fixpoint}
 instead of \texttt{Function}, but the scheme will not be generated.
 
 This error happens generally when: 
@@ -1427,10 +1427,10 @@ given below.
 \comindex{Function}
 }
 
-Defines  the  not  recursive  function  \ident\ as  if  declared  with
-\texttt{Definition}.    Three  induction   schemes  {\tt\ident\_rect},
-{\tt\ident\_rec}   and  {\tt\ident\_ind}   are   generated  (see   the
-documentation of {\tt  Inductive} \ref{Inductive}), which reflect the
+Defines the not recursive function \ident\ as if declared with
+\texttt{Definition}.  Three elimination schemes {\tt\ident\_rect},
+{\tt\ident\_rec} and {\tt\ident\_ind} are generated (see the
+documentation of {\tt Inductive} \ref{Inductive}), which reflect the
 pattern matching structure of \term$_0$.
 
 
@@ -1485,7 +1485,7 @@ proof that the ordering relation is well founded.
 The fixpoint equality  \texttt{\ident\_equation}, which is not trivial
 to prove in this case, is automatically generated and proved, together
 with three  induction schemes {\tt\ident\_rect},  {\tt\ident\_rec} and
-{\tt\ident\_ind}  are   generated  (see  the   documentation  of  {\tt
+{\tt\ident\_ind} as explained above  (see  the   documentation  of  {\tt
   Inductive} \ref{Inductive}), which  reflect the recursive structure
 of \term$_0$.
 
-- 
cgit v1.2.3