diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 30ba4acf0..75ba90f03 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2023,6 +2023,7 @@ makes use of a principle generated by \texttt{Function} \begin{coq_eval} Reset Initial. +Import Nat. \end{coq_eval} \begin{coq_example} Functional Scheme minus_ind := Induction for minus Sort Prop. @@ -2042,7 +2043,7 @@ you want to write implicit arguments explicitly. \Rem Parentheses over \qualid \dots \term$_n$ are mandatory. \Rem \texttt{functional induction (f x1 x2 x3)} is actually a wrapper -for \texttt{induction x1 x2 x3 (f x1 x2 x3) using \qualid} followed by +for \texttt{induction x1, x2, x3, (f x1 x2 x3) using \qualid} followed by a cleaning phase, where {\qualid} is the induction principle registered for $f$ (by the \texttt{Function} (see Section~\ref{Function}) or \texttt{Functional Scheme} (see Section~\ref{FunScheme}) command) |