diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 24824b841..3e2c17245 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1394,7 +1394,7 @@ Qed. The \emph{experimental} tactic \texttt{functional induction} performs case analysis and induction following the definition of a (not mutually recursive) function. It makes use of principle -generated by \texttt{Function}\ref{??}. +generated by \texttt{Function}\ref{Function}. \begin{coq_eval} Reset Initial. |