diff options
Diffstat (limited to 'doc/refman/RefMan-tacex.tex')
| -rw-r--r-- | doc/refman/RefMan-tacex.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index 951de0cd72..9837c8ba3b 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -363,7 +363,7 @@ Qed. \end{coq_example*} \Rem There is a difference between obtaining an induction scheme for a -function by using \texttt{Function} (section~\ref{Function}) and by +function by using \texttt{Function} (see Section~\ref{Function}) and by using \texttt{Functional Scheme} after a normal definition using \texttt{Fixpoint} or \texttt{Definition}. See \ref{Function} for details. |