From c5492fd8e8ff8a15349ec48dbcc784ffc9746e0a Mon Sep 17 00:00:00 2001
From: jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 17 May 2006 10:05:24 +0000
Subject: updating Function documentation

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

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 043de5408..3f29f5e91 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1333,6 +1333,7 @@ Function plus (n m : nat) {struct n} : nat :=
 \term$_0$ must be build as an imbrication of pattern matchings
 (\texttt{match...with}) with $\lambda$-abstraction and applications only
 \emph{at the end} of each branch.
+For now dependent cases are not treated.
 
 \SeeAlso{\ref{FunScheme},\ref{FunScheme-examples},\ref{FunInduction}}
 
@@ -1345,9 +1346,11 @@ given below.
 \comindex{Function}
 }
 
-Defines the not recursive function \ident\ as if declared with
-\texttt{Definition}. An induction scheme {\tt\ident\_ind} is generated, which
-reflects the pattern matching structure of \term$_0$.
+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
+pattern matching structure of \term$_0$.
 
 
 \subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
@@ -1355,11 +1358,12 @@ reflects the pattern matching structure of \term$_0$.
 \comindex{Function}
 }
 
-Defines the structural recursive function \ident\ as if declared with
-\texttt{Fixpoint} . An induction scheme {\tt\ident\_ind} is
-generated, which reflects the recursive structure of \term$_0$. When
-there is only one parameter, {\tt \{struct} \ident$_0${\tt\}} can be
-omitted.
+Defines the structural recursive  function \ident\ as if declared with
+\texttt{Fixpoint}   .  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
+recursive structure  of \term$_0$. When  there is only  one parameter,
+{\tt \{struct} \ident$_0${\tt\}} can be omitted.
 
 \subsubsection{\tt Function {\ident} {\binder$_1$}\ldots{\binder$_n$}
  {\tt \{}{\tt measure \term$_1$} \ident$_0${\tt\}} : type$_0$ := \term$_0$.
@@ -1397,24 +1401,26 @@ proof that the ordering relation is well founded.
 
 %Completer sur measure et wf
 
-The fixpoint equality \texttt{\ident\_eq}, which is not trivial to
-prove in this case, is automatically generated and proved, together
-with an induction scheme {\tt\ident\_ind}, which reflects the recursive
-structure of \term$_0$.
+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
+  Inductive} \ref{Inductive}), which  reflect the recursive structure
+of \term$_0$.
 
 
 
 %Complete!!
 The way this recursive function is defined is the subject of several
-papers by Yves Bertot, Julien forest, David Pichardie.
+papers by Yves Bertot, Julien Forest, David Pichardie.
 
 %Exemples ok ici
 
 \bigskip
 
 \noindent {\bf Remark: } Proof obligations are presented as several
-subgoals. These subgoals are independent which means that in order to
-abort them you will have to abort each separately.
+subgoals belonging to a Lemma {\ident}{\tt\_tcc}. % These subgoals are independent which means that in order to
+% abort them you will have to abort each separately.
 
 
 
-- 
cgit v1.2.3