diff options
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 970347422c..f6baa44555 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -717,7 +717,7 @@ 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 := + Function wrong (C:nat) : nat := List.hd(List.map wrong (C::nil)). \end{coq_example*} |