diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-28 17:10:12 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-28 17:10:12 +0000 |
| commit | a46abe18b97fda1f56d8cef16882924542e9c1e9 (patch) | |
| tree | 198d4ef560f098bdab1ad808b47d2f1f5420659f /doc/refman/RefMan-tac.tex | |
| parent | c864695069da8f83a488261d9e842bfba970d114 (diff) | |
Continue l'écriture de la doc de "Function". Pas fini, manque:
- relecture par YB et JF
- adaptation de la partie functional induction
- écriture de la partie functional inversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8770 85f007b7-540e-0410-9357-904b9bb8a0f7
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. |