diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 253eb7f01b..2bab04e90a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2113,13 +2113,15 @@ The tactic \texttt{functional induction} performs case analysis and induction following the definition of a function. It makes use of a principle generated by \texttt{Function} (see Section~\ref{Function}) or \texttt{Functional Scheme} -(see Section~\ref{FunScheme}). +(see Section~\ref{FunScheme}). Note that this tactic is only available +after a {\tt Require Import FunInd}. \begin{coq_eval} Reset Initial. Import Nat. \end{coq_eval} \begin{coq_example} +Require Import FunInd. Functional Scheme minus_ind := Induction for minus Sort Prop. Check minus_ind. Lemma le_minus (n m:nat) : n - m <= n. @@ -4797,6 +4799,7 @@ that performs inversion on hypothesis {\ident} of the form \texttt{\qualid\ \term$_1$\dots\term$_n$\ = \term} or \texttt{\term\ = \qualid\ \term$_1$\dots\term$_n$} where \qualid\ must have been defined using \texttt{Function} (see Section~\ref{Function}). +Note that this tactic is only available after a {\tt Require Import FunInd}. \begin{ErrMsgs} \item \errindex{Hypothesis {\ident} must contain at least one Function} |