diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-07 21:28:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-07 21:28:49 +0100 |
| commit | 7e4241a6aec516b8b28bc0c6f2125c5960b909e7 (patch) | |
| tree | 9525bef5131f94f8ae01b2ddd0b87c980baf9ef9 | |
| parent | 2393592c9e5a609e19a96250e2e7588c1aa28ca9 (diff) | |
Fixing doc of Functional Induction.
| -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) |