Correction in Function documentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12995 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 01df199ab9..503167987d 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -675,7 +675,15 @@ Function plus (n m : nat) {struct n} : nat :=
 \paragraph[Limitations]{Limitations\label{sec:Function-limitations}}
 \term$_0$ must be build as a \emph{pure pattern-matching tree}
 (\texttt{match...with}) with applications only \emph{at the end} of
-each branch.  For now dependent cases are not treated.
+each branch.  
+
+Function does not support partial application of the function being defined. Thus, the following example cannot be accepted due to the presence of partial application of \ident{wrong} into the body of \ident{wrong}~:
+\begin{coq_example*}
+  Function wrong (C:nat) {\ldots} : nat := 
+    List.hd(List.map wrong (C::nil)).
+\end{coq_example*}
+
+For now dependent cases are not treated for non structurally terminating functions.